(DCL PATH-HYPS NIL) [ 0.0 0.0 0.0 ] PATH-HYPS (DCL GLOBAL-HYPS NIL) [ 0.0 0.0 0.0 ] GLOBAL-HYPS (ADD-AXIOM PATH-HYPS-BOOLEAN (REWRITE) (OR (TRUEP (PATH-HYPS)) (FALSEP (PATH-HYPS)))) WARNING: Note that the proposed lemma PATH-HYPS-BOOLEAN is to be stored as one type prescription rule, zero compound recognizer rules, zero linear rules, and zero replacement rules. [ 0.0 0.0 0.0 ] PATH-HYPS-BOOLEAN (ADD-AXIOM GLOBAL-HYPS-BOOLEAN (REWRITE) (OR (TRUEP (GLOBAL-HYPS)) (FALSEP (GLOBAL-HYPS)))) WARNING: Note that the proposed lemma GLOBAL-HYPS-BOOLEAN is to be stored as one type prescription rule, zero compound recognizer rules, zero linear rules, and zero replacement rules. [ 0.0 0.0 0.0 ] GLOBAL-HYPS-BOOLEAN (DCL SQ (I)) [ 0.0 0.0 0.0 ] SQ (DCL START NIL) [ 0.0 0.0 0.0 ] START (DCL I (STATE)) [ 0.0 0.0 0.0 ] I (DCL ISQRT (STATE)) [ 0.0 0.0 0.0 ] ISQRT (DCL BEGIN NIL) [ 0.0 0.0 0.0 ] BEGIN (DCL NEXT (STATE)) [ 0.0 0.0 0.0 ] NEXTNEXTNEXT((ADD-AXIOM DCL-START NIL '*1*TRUE) (DCL A (STATE)) (DCL MAXI (STATE)))