定義40 xは公理IVから得られる"論理式"である (define (IsAxiomIV [x : GForm]) (∃ u v y n <= x (and (IsVarType (gsymbol+ u) (+ n 1)) (IsVarType (gsymbol+ v) n) (IsForm (gsequence+ y)) (not (IsFree (gsymbol+ u) (gform+ y))) (= x (Exists (gsymbo…