#|
 Copyright (C) 1994 by Natarajan Shankar.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Natarajan Shankar PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Natarajan Shankar BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

(BOOT-STRAP THM)

;Annotated script for mechanical proof of the Tautology theorem.
;Proof involves - 
;Definition of proof-checker for Schoenfield's FOL.
;Proof of several derived inference rules, primarily the
;subset lemma.
;Definition of tautology-checker.
;Every tautology has a proof.
;Correctness of tautology-checker - every tautology is
;always logically-true, and all logical-truths are tautologies.
;First, functions, variables and predicate symbols.
(DEFN FUNCTION
     (FN)
     (AND (EQUAL FN (LIST 'F (CADR FN) (CADDR FN)))
          (NUMBERP (CADR FN))
          (NUMBERP (CADDR FN))))
(DEFN VARIABLE
     (X)
     (AND (EQUAL X (LIST 'X (CADR X)))
          (NUMBERP (CADR X))))
(DEFN PREDICATE
     (P)
     (OR (AND (EQUAL P (LIST 'P (CADR P) (CADDR P)))
              (NUMBERP (CADR P))
              (NUMBERP (CADDR P)))
         (EQUAL P 'EQUAL)))
(DEFN DEGREE (FN) (IF (EQUAL FN 'EQUAL) 2 (CADDR FN)))
(DEFN INDEX (FN) (CADR FN))
(DEFN FUNC-PRED
     (X)
     (OR (FUNCTION X)
         (PREDICATE X)))
(DEFN V (X) (LIST 'X (FIX X)))
(PROVE-LEMMA NUMBERP-FIX (REWRITE) (NUMBERP (FIX X)))
(PROVE-LEMMA VARIABLE-V (REWRITE) (VARIABLE (V X)))
(DEFN FN (X Y) (LIST 'F (FIX X) (FIX Y)))
(DEFN P (X Y) (LIST 'P (FIX X) (FIX Y)))
(PROVE-LEMMA FUNCTION-FN (REWRITE) (FUNCTION (FN X Y)))
(PROVE-LEMMA PREDICATE-P (REWRITE) (PREDICATE (P X Y)))
;quantifer, there exists.
(DEFN QUANTIFIER (X) (EQUAL X 'FORSOME))
(DEFN UNION
     (X Y)
     (IF (LISTP X) (IF (MEMBER (CAR X) Y) (UNION (CDR X) Y) (CONS (CAR X) (UNION (CDR X) Y))) Y))
(TOGGLE G0223 VARIABLE T)
(TOGGLE G0224 QUANTIFIER T)
(PROVE-LEMMA PREDICATE-F-EQUAL (REWRITE) (PREDICATE 'EQUAL))
(TOGGLE G0225 FUNCTION T)
(TOGGLE G0226 PREDICATE T)
(DEFN APPEND (X Y) (IF (LISTP X) (CONS (CAR X) (APPEND (CDR X) Y)) Y))
(DEFN DELETE
     (X Y)
     (IF (LISTP Y) (IF (EQUAL X (CAR Y)) (DELETE X (CDR Y)) (CONS (CAR Y) (DELETE X (CDR Y)))) Y))
(PROVE-LEMMA NOT-MEMBER-DELETE (REWRITE) (NOT (MEMBER X (DELETE X Y))))
;returns list of free variables in EXP.
(DEFN COLLECT-FREE
     (EXP FLG)
     (IF (LISTP EXP)
         (IF (EQUAL FLG T)
             (IF (VARIABLE EXP)
                 (CONS EXP NIL)
                 (IF (AND (QUANTIFIER (CAR EXP))
                          (LISTP (CDR EXP)))
                     (DELETE (CADR EXP) (COLLECT-FREE (CDDR EXP) 'LIST))
                     (IF (OR (FUNC-PRED (CAR EXP))
                             (EQUAL (CAR EXP) 'NOT)
                             (EQUAL (CAR EXP) 'OR))
                         (COLLECT-FREE (CDR EXP) 'LIST)
                         NIL)))
             (APPEND (COLLECT-FREE (CAR EXP) T) (COLLECT-FREE (CDR EXP) 'LIST)))
         NIL))
(DEFN SENTENCE (EXP) (EQUAL (COLLECT-FREE EXP T) NIL))
;returns bound variables in EXP that surround free occurrences of VAR.
(DEFN COVERING
     (EXP VAR FLG)
     (IF (LISTP EXP)
         (IF (EQUAL FLG T)
             (IF (VARIABLE EXP)
                 NIL
                 (IF (AND (QUANTIFIER (CAR EXP))
                          (LISTP (CDR EXP)))
                     (IF (EQUAL (CADR EXP) VAR)
                         NIL
                         (IF (MEMBER VAR (COLLECT-FREE (CDDR EXP) 'LIST))
                             (CONS (CADR EXP) (COVERING (CDDR EXP) VAR 'LIST))
                             NIL))
                     (IF (OR (FUNC-PRED (CAR EXP))
                             (EQUAL (CAR EXP) 'NOT)
                             (EQUAL (CAR EXP) 'OR))
                         (COVERING (CDR EXP) VAR 'LIST)
                         NIL)))
             (APPEND (COVERING (CAR EXP) VAR T) (COVERING (CDR EXP) VAR 'LIST)))
         NIL))
;X and Y are disjoint.
(DEFN NIL-INTERSECT
     (X Y)
     (IF (LISTP X)
         (AND (NOT (MEMBER (CAR X) Y))
              (NIL-INTERSECT (CDR X) Y))
         T))
;TERM is free for VAR in EXP.
(DEFN FREE-FOR (EXP VAR TERM FLG) (NIL-INTERSECT (COVERING EXP VAR FLG) (COLLECT-FREE TERM T)))
(DEFN F-EQUAL (X Y) (LIST 'EQUAL X Y))
(DEFN F-NOT (X) (LIST 'NOT X))
(DEFN F-OR (X Y) (LIST 'OR X Y))
(DEFN FORSOME (X Y) (LIST 'FORSOME X Y))
(DEFN F-AND (X Y) (F-NOT (F-OR (F-NOT X) (F-NOT Y))))
(DEFN F-IMPLIES (X Y) (F-OR (F-NOT X) Y))
(DEFN FORALL (VAR EXP) (F-NOT (FORSOME VAR (F-NOT EXP))))
(DEFN F-IFF (X Y) (F-AND (F-IMPLIES X Y) (F-IMPLIES Y X)))
(DEFN VAR-LIST
     (LIST N)
     (IF (ZEROP N)
         (EQUAL LIST NIL)
         (AND (VARIABLE (CAR LIST))
              (VAR-LIST (CDR LIST) (SUB1 N)))))
(DEFN VAR-SET
     (LIST N)
     (IF (ZEROP N)
         (EQUAL LIST NIL)
         (AND (VARIABLE (CAR LIST))
              (NOT (MEMBER (CAR LIST) (CDR LIST)))
              (VAR-SET (CDR LIST) (SUB1 N)))))
;Recognizer for terms.
(DEFN TERMP
     (EXP FLG COUNT)
     (IF (EQUAL FLG T)
         (IF (NLISTP EXP)
             F
             (OR (VARIABLE EXP)
                 (AND (FUNCTION (CAR EXP))
                      (TERMP (CDR EXP) 'LIST (DEGREE (CAR EXP))))))
         (IF (OR (NLISTP EXP)
                 (ZEROP COUNT))
             (AND (EQUAL EXP NIL)
                  (ZEROP COUNT))
             (AND (TERMP (CAR EXP) T 0)
                  (TERMP (CDR EXP) 'LIST (SUB1 COUNT))))))
(DEFN ARG1 (X) (CADR X))
(DEFN ARG2 (X) (CADDR X))
;EXP is an atom, pred. symbol followed by list of terms.
(DEFN ATOMP
     (EXP)
     (AND (PREDICATE (CAR EXP))
          (TERMP (CDR EXP) 'LIST (DEGREE (CAR EXP)))))
(TOGGLE G0253 ATOMP T)
;EXP is a formula
(DEFN FORMULA
     (EXP FLG COUNT)
     (IF (EQUAL FLG T)
         (IF (NLISTP EXP)
             F
             (OR (ATOMP EXP)
                 (AND (EQUAL (CAR EXP) 'NOT)
                      (FORMULA (CDR EXP) 'LIST 1))
                 (AND (EQUAL (CAR EXP) 'OR)
                      (FORMULA (CDR EXP) 'LIST 2))
                 (AND (EQUAL (CAR EXP) 'FORSOME)
                      (VARIABLE (CADR EXP))
                      (FORMULA (CDDR EXP) 'LIST 1))))
         (IF (OR (NLISTP EXP)
                 (ZEROP COUNT))
             (AND (EQUAL EXP NIL)
                  (ZEROP COUNT))
             (AND (FORMULA (CAR EXP) T 0)
                  (FORMULA (CDR EXP) 'LIST (SUB1 COUNT))))))
;Result of substituting TERM for VAR in EXP.
(DEFN SUBST
     (EXP VAR TERM FLG)
     (IF (LISTP EXP)
         (IF (EQUAL FLG T)
             (IF (VARIABLE EXP)
                 (IF (EQUAL EXP VAR) TERM EXP)
                 (IF (AND (QUANTIFIER (CAR EXP))
                          (LISTP (CDR EXP)))
                     (IF (EQUAL (CADR EXP) VAR)
                         EXP
                         (CONS (CAR EXP) (CONS (CADR EXP) (SUBST (CDDR EXP) VAR TERM 'LIST))))
                     (IF (OR (FUNC-PRED (CAR EXP))
                             (EQUAL (CAR EXP) 'NOT)
                             (EQUAL (CAR EXP) 'OR))
                         (CONS (CAR EXP) (SUBST (CDR EXP) VAR TERM 'LIST))
                         EXP)))
             (CONS (SUBST (CAR EXP) VAR TERM T) (SUBST (CDR EXP) VAR TERM 'LIST)))
         EXP))
(DEFN NEG
     (EXP1 EXP2)
     (OR (EQUAL EXP1 (F-NOT EXP2))
         (EQUAL EXP2 (F-NOT EXP1))))
(DEFN CONC
     (PF FLG)
     (IF (NLISTP PF)
         NIL
         (IF (EQUAL FLG T) (CADDR PF) (CONS (CONC (CAR PF) T) (CONC (CDR PF) 'LIST)))))
(DEFN SUBSET
     (X Y)
     (IF (LISTP X)
         (AND (MEMBER (CAR X) Y)
              (SUBSET (CDR X) Y))
         T))
(DEFN SET-EQUAL
     (X Y)
     (AND (SUBSET X Y)
          (SUBSET Y X)))
;The axioms: propositional, substitution, identity, equality for functions and predicates.
(DEFN PROP-AXIOM (EXP) (F-OR (F-NOT EXP) EXP))
(DEFN SUBST-AXIOM (EXP VAR TERM) (F-IMPLIES (SUBST EXP VAR TERM T) (FORSOME VAR EXP)))
(DEFN IDENT-AXIOM (VAR) (F-EQUAL VAR VAR))
(DEFN PAIREQUALS
     (VARS1 VARS2 EXP)
     (IF (LISTP VARS1)
         (F-IMPLIES (F-EQUAL (CAR VARS1) (CAR VARS2)) (PAIREQUALS (CDR VARS1) (CDR VARS2) EXP))
         EXP))
(DEFN EQUAL-AXIOM2
     (VARS1 VARS2 PR)
     (PAIREQUALS VARS1 VARS2 (F-IMPLIES (CONS PR VARS1) (CONS PR VARS2))))
(DEFN ASSUME
     (EXP LIST FLG)
     (IF (LISTP LIST)
         (IF (AND (EQUAL (CAAAR LIST) FLG)
                  (EQUAL EXP (CADAR LIST)))
             (CDR LIST)
             (ASSUME EXP (CDR LIST) FLG))
         F))
;Proof-constructors
(DEFN PROP-AXIOM-PROOF (EXP) (LIST 'AXIOM (LIST 'PROP-AXIOM EXP) (PROP-AXIOM EXP)))
(DEFN SUBST-AXIOM-PROOF
     (EXP VAR TERM)
     (LIST 'AXIOM (LIST 'SUBST-AXIOM EXP VAR TERM) (SUBST-AXIOM EXP VAR TERM)))
(DEFN IDENT-AXIOM-PROOF (VAR) (LIST 'AXIOM (LIST 'IDENT-AXIOM VAR) (F-EQUAL VAR VAR)))
(DEFN EQUAL-AXIOM1
     (VARS1 VARS2 FN)
     (PAIREQUALS VARS1 VARS2 (F-EQUAL (CONS FN VARS1) (CONS FN VARS2))))
(DEFN EQUAL-AXIOM1-PROOF
     (FN VARS1 VARS2)
     (LIST 'AXIOM (LIST 'EQUAL-AXIOM1 FN VARS1 VARS2) (EQUAL-AXIOM1 VARS1 VARS2 FN)))
(DEFN EQUAL-AXIOM2-PROOF
     (PR VARS1 VARS2)
     (LIST 'AXIOM (LIST 'EQUAL-AXIOM2 PR VARS1 VARS2) (EQUAL-AXIOM2 VARS1 VARS2 PR)))
(DEFN EXPAN-PROOF (A B PF) (LIST 'RULE (LIST 'EXPAN A B) (F-OR A B) PF))
(DEFN CONTRAC-PROOF (A PF) (LIST 'RULE (LIST 'CONTRAC A) A PF))
(DEFN ASSOC-PROOF (A B C PF) (LIST 'RULE (LIST 'ASSOC A B C) (F-OR (F-OR A B) C) PF))
(DEFN CUT-PROOF (A B C PF1 PF2) (LIST 'RULE (LIST 'CUT A B C) (F-OR B C) (LIST PF1 PF2)))
(DEFN FORSOME-INTRO-PROOF
     (VAR A B PF)
     (LIST 'RULE (LIST 'E-INTRO VAR A B) (F-IMPLIES (FORSOME VAR A) B) PF))
(TOGGLE G2737 ATOMP NIL)
(DEFN HINT1 (PF)(CAADR PF))
(DEFN HINT2 (PF)(CADADR PF))
(DEFN HINT3 (PF)(CADDADR PF))
(DEFN HINT4 (PF)(CADDDADR PF))
(DEFN SUB-PROOF (PF)(CADDDR PF))
;The proof-checker, PF is a proof.
(DEFN
PRF
(PF)
(IF (NLISTP PF)
    F
    (IF (EQUAL (CAR PF) 'AXIOM)
        (IF (EQUAL (HINT1 PF) 'PROP-AXIOM)
            (AND (FORMULA (HINT2 PF) T 0)
                 (EQUAL PF (PROP-AXIOM-PROOF (HINT2 PF))))
            (IF (EQUAL (HINT1 PF) 'SUBST-AXIOM)
                (AND (FORMULA (HINT2 PF) T 0)
                     (VARIABLE (HINT3 PF))
                     (TERMP (HINT4 PF) T 0)
                     (FREE-FOR (HINT2 PF) (HINT3 PF) (HINT4 PF) T)
                     (EQUAL PF (SUBST-AXIOM-PROOF (HINT2 PF) (HINT3 PF) (HINT4 PF))))
                (IF (EQUAL (HINT1 PF) 'IDENT-AXIOM)
                    (AND (VARIABLE (HINT2 PF))
                         (EQUAL PF (IDENT-AXIOM-PROOF (HINT2 PF))))
                    (IF (EQUAL (HINT1 PF) 'EQUAL-AXIOM1)
                        (AND (FUNCTION (HINT2 PF))
                             (VAR-LIST (HINT3 PF) (DEGREE (HINT2 PF)))
                             (VAR-LIST (HINT4 PF) (DEGREE (HINT2 PF)))
                             (EQUAL PF
                                    (EQUAL-AXIOM1-PROOF (HINT2 PF)
                                                        (HINT3 PF)
                                                        (HINT4 PF))))
                        (IF (EQUAL (HINT1 PF) 'EQUAL-AXIOM2)
                            (AND (PREDICATE (HINT2 PF))
                                 (VAR-LIST (HINT3 PF) (DEGREE (HINT2 PF)))
                                 (VAR-LIST (HINT4 PF) (DEGREE (HINT2 PF)))
                                 (EQUAL PF
                                        (EQUAL-AXIOM2-PROOF (HINT2 PF)
                                                            (HINT3 PF)
                                                            (HINT4 PF))))
                            F)))))
                (IF (EQUAL (CAR PF) 'RULE)
                    (IF (EQUAL (HINT1 PF) 'EXPAN)
                        (AND (FORMULA (HINT2 PF) T 0)
                             (EQUAL PF (EXPAN-PROOF (HINT2 PF) (HINT3 PF) (SUB-PROOF PF)))
                             (EQUAL (CONC (SUB-PROOF PF) T) (HINT3 PF))
                             (PRF (SUB-PROOF PF)))
                        (IF (EQUAL (HINT1 PF) 'CONTRAC)
                            (AND (EQUAL PF (CONTRAC-PROOF (HINT2 PF) (SUB-PROOF PF)))
                                 (EQUAL (CONC (SUB-PROOF PF) T) (F-OR (HINT2 PF) (HINT2 PF)))
                                 (PRF (SUB-PROOF PF)))
                            (IF (EQUAL (HINT1 PF) 'ASSOC)
                                (AND (EQUAL PF
                                            (ASSOC-PROOF (HINT2 PF)
                                                         (HINT3 PF)
                                                         (HINT4 PF)
                                                         (SUB-PROOF PF)))
                                     (EQUAL (CONC (SUB-PROOF PF) T)
                                            (F-OR (HINT2 PF)
                                                  (F-OR (HINT3 PF) (HINT4 PF))))
                                     (PRF (SUB-PROOF PF)))
                                (IF (EQUAL (HINT1 PF) 'CUT)
                                    (AND (EQUAL PF
                                                (CUT-PROOF (HINT2 PF)
                                                           (HINT3 PF)
                                                           (HINT4 PF)
                                                           (CAR (SUB-PROOF PF))
                                                           (CADR (SUB-PROOF PF))))
                                         (EQUAL (CONC (SUB-PROOF PF) 'LIST)
                                                (LIST (F-OR (HINT2 PF) (HINT3 PF))
                                                      (F-OR (F-NOT (HINT2 PF))
                                                            (HINT4 PF))))
                                         (PRF (CAR (SUB-PROOF PF)))
                                         (PRF (CADR (SUB-PROOF PF))))
                                    (IF (EQUAL (HINT1 PF) 'E-INTRO)
                                        (AND (VARIABLE (HINT2 PF))
                                             (EQUAL PF
                                                    (FORSOME-INTRO-PROOF (HINT2 PF)
                                                                         (HINT3 PF)
                                                                         (HINT4 PF)
                                                                         (SUB-PROOF PF)))
                                             (NOT (MEMBER (HINT2 PF)
                                                          (COLLECT-FREE (HINT4 PF)
                                                                        T)))
                                             (EQUAL (CONC (SUB-PROOF PF) T)
                                                    (F-IMPLIES (HINT3 PF)
                                                               (HINT4 PF)))
                                             (PRF (SUB-PROOF PF)))
                                        F)))))
                    F))))
(PROVE-LEMMA FORMULA-OR-REDUC
            (REWRITE)
            (EQUAL (FORMULA (LIST 'OR A B) T 0)
                   (AND (FORMULA A T 0)
                        (FORMULA B T 0))))
(PROVE-LEMMA FORMULA-NOT-REDUC (REWRITE) (EQUAL (FORMULA (LIST 'NOT A) T 0) (FORMULA A T 0)))
(PROVE-LEMMA FORMULA-FORSOME-REDUC
            (REWRITE)
            (EQUAL (FORMULA (LIST 'FORSOME X A) T 0)
                   (AND (VARIABLE X)
                        (FORMULA A T 0))))
;PF is a valid proof of EXP.
(DEFN PROVES
     (PF EXP)
     (AND (EQUAL (CONC PF T) EXP)
          (FORMULA EXP T 0)
          (PRF PF)))
(PROVE-LEMMA PROVES-IS-FORMULA (REWRITE) (IMPLIES (PROVES PF EXP) (FORMULA EXP T 0)))
(PROVE-LEMMA PROVES-IS-FORMULA-AGAIN
            (REWRITE)
            (IMPLIES (NOT (FORMULA EXP T 0)) (NOT (PROVES PF EXP)))
            ((DISABLE FORMULA)))
;Getting rid of PRF by lemmas.
(PROVE-LEMMA PROP-AXIOM-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA EXP T 0)
                          (EQUAL CONCL (F-OR (F-NOT EXP) EXP)))
                     (PROVES (PROP-AXIOM-PROOF EXP) CONCL)))
(PROVE-LEMMA SUBST-AXIOM-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA CONCL T 0)
                          (VARIABLE VAR)
                          (TERMP TERM T 0)
                          (FREE-FOR EXP VAR TERM T)
                          (EQUAL CONCL (SUBST-AXIOM EXP VAR TERM)))
                     (PROVES (SUBST-AXIOM-PROOF EXP VAR TERM) CONCL))
            ((DISABLE FREE-FOR)))
(PROVE-LEMMA EQUAL-AXIOM1-PROVES
            (REWRITE)
            (IMPLIES (AND (FUNCTION FN)
                          (VAR-LIST VARS1 (DEGREE FN))
                          (VAR-LIST VARS2 (DEGREE FN))
                          (FORMULA CONCL T 0)
                          (EQUAL CONCL (EQUAL-AXIOM1 VARS1 VARS2 FN)))
                     (PROVES (EQUAL-AXIOM1-PROOF FN VARS1 VARS2) CONCL)))
(PROVE-LEMMA EQUAL-AXIOM2-PROVES
            (REWRITE)
            (IMPLIES (AND (PREDICATE PR)
                          (VAR-LIST VARS1 (DEGREE PR))
                          (VAR-LIST VARS2 (DEGREE PR))
                          (FORMULA CONCL T 0)
                          (EQUAL CONCL (EQUAL-AXIOM2 VARS1 VARS2 PR)))
                     (PROVES (EQUAL-AXIOM2-PROOF PR VARS1 VARS2) CONCL)))
(PROVE-LEMMA IDENT-AXIOM-PROVES
            (REWRITE)
            (IMPLIES (AND (VARIABLE VAR)
                          (EQUAL CONCL (IDENT-AXIOM VAR))
                          (FORMULA CONCL T 0))
                     (PROVES (IDENT-AXIOM-PROOF VAR) CONCL)))
(PROVE-LEMMA EXPAN-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA A T 0)
                          (PROVES PF B)
                          (EQUAL CONCL (F-OR A B)))
                     (PROVES (EXPAN-PROOF A B PF) CONCL)))
(PROVE-LEMMA CONTRAC-PROOF-PROVES
            (REWRITE)
            (IMPLIES (PROVES PF (F-OR A A)) (PROVES (CONTRAC-PROOF A PF) A)))
(PROVE-LEMMA ASSOC-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF (F-OR A (F-OR B C)))
                          (EQUAL CONCL (F-OR (F-OR A B) C)))
                     (PROVES (ASSOC-PROOF A B C PF) CONCL)))
(PROVE-LEMMA CUT-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF1 (F-OR A B))
                          (PROVES PF2 (F-OR (F-NOT A) C))
                          (EQUAL CONCL (F-OR B C)))
                     (PROVES (CUT-PROOF A B C PF1 PF2) CONCL)))
;disabling the proof-constructors since the lemmas above show they work.
(TOGGLE G2752 PROP-AXIOM-PROOF T)
(TOGGLE G2753 SUBST-AXIOM-PROOF T)
(TOGGLE G2754 EQUAL-AXIOM1-PROOF T)
(TOGGLE G2755 EQUAL-AXIOM2-PROOF T)
(TOGGLE G2756 IDENT-AXIOM-PROOF T)
(TOGGLE G2759 EXPAN-PROOF T)
(TOGGLE G2760 CONTRAC-PROOF T)
(TOGGLE G2761 ASSOC-PROOF T)
(TOGGLE G2762 CUT-PROOF T)
(PROVE-LEMMA FORSOME-INTRO-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF (F-IMPLIES A B))
                          (NOT (MEMBER VAR (COLLECT-FREE B T)))
                          (VARIABLE VAR)
                          (EQUAL A-PRIME (F-IMPLIES (FORSOME VAR A) B)))
                     (PROVES (FORSOME-INTRO-PROOF VAR A B PF) A-PRIME))
            ((DISABLE COLLECT-FREE FORMULA)))
(TOGGLE G2763 FORSOME-INTRO-PROOF T)
(TOGGLE G2764 PRF T)
(TOGGLE G2765 PROVES T)
(DEFN COMMUT-PROOF (A B PF) (CUT-PROOF A B A PF (PROP-AXIOM-PROOF A)))
;The first derived inference rule - commutativity of disjunction.
(PROVE-LEMMA COMMUT-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF (F-OR A B))
                          (FORMULA (F-OR A B) T 0)
                          (EQUAL CONCL (F-OR B A)))
                     (PROVES (COMMUT-PROOF A B PF) CONCL)))
(TOGGLE G2766 COMMUT-PROOF T)
;Modus Ponens.
(DEFN DETACH-PROOF
     (A B PF1 PF2)
     (CONTRAC-PROOF B (CUT-PROOF A B B (COMMUT-PROOF B A (EXPAN-PROOF B A PF1)) PF2)))
(PROVE-LEMMA DETACH-PROOF-PROVES1
            (REWRITE)
            (IMPLIES (AND (PROVES PF1 A)
                          (PROVES PF2 (F-IMPLIES A B))
                          (FORMULA B T 0))
                     (PROVES (DETACH-PROOF A B PF1 PF2) B))
            ((DISABLE FORMULA)))
(TOGGLE G2767 DETACH-PROOF T)
(DEFN PROVES-LIST
     (PFLIST EXPLIST)
     (IF (NLISTP EXPLIST)
         (EQUAL PFLIST NIL)
         (AND (PROVES (CAR PFLIST) (CAR EXPLIST))
              (PROVES-LIST (CDR PFLIST) (CDR EXPLIST)))))
(DEFN LIST-IMPLIES
     (LIST CONC)
     (IF (NLISTP LIST)
         CONC
         (IF (NLISTP (CDR LIST))
             (F-IMPLIES (CAR LIST) CONC)
             (F-IMPLIES (CAR LIST) (LIST-IMPLIES (CDR LIST) CONC)))))
(DEFN LIST-DETACH-PROOF
     (ALIST B PFLIST PF2)
     (IF (NLISTP ALIST)
         PF2
         (IF (NLISTP (CDR ALIST))
             (DETACH-PROOF (CAR ALIST) B (CAR PFLIST) PF2)
             (LIST-DETACH-PROOF (CDR ALIST)
                                B
                                (CDR PFLIST)
                                (DETACH-PROOF (CAR ALIST)
                                              (LIST-IMPLIES (CDR ALIST) B)
                                              (CAR PFLIST)
                                              PF2)))))
;Chained Modus Ponens.
(PROVE-LEMMA DETACH-LIST-IMPLIES
            (REWRITE)
            (IMPLIES (AND (LIST C)
                          (PROVES PF A)
                          (PROVES PF2 (LIST-IMPLIES (CONS A C) B))
                          (FORMULA A T 0)
                          (FORMULA (LIST-IMPLIES C B) T 0))
                     (PROVES (DETACH-PROOF A (LIST-IMPLIES C B) PF PF2)
                             (LIST-IMPLIES C B)
                            )))
(PROVE-LEMMA FORMULA-LIST-IMPLIES
            NIL
            (IMPLIES (AND (FORMULA (LIST-IMPLIES ALIST B) T 0)
                          (LISTP ALIST))
                     (FORMULA (LIST-IMPLIES (CDR ALIST) B) T 0)))
(PROVE-LEMMA
DETACH-RULE-CORR
(REWRITE)
(IMPLIES (AND (PROVES-LIST PFLIST ALIST)
              (PROVES PF2 (LIST-IMPLIES ALIST B))
              (FORMULA B T 0))
         (PROVES (LIST-DETACH-PROOF ALIST B PFLIST PF2) B))
((INDUCT (LIST-DETACH-PROOF ALIST B PFLIST PF2)) (USE (DETACH-LIST-IMPLIES (A (CAR ALIST))
                                                                           (C (CDR ALIST))
                                                                           (PF (CAR PFLIST)))
                                                      (FORMULA-LIST-IMPLIES))))
(TOGGLE G0220 LIST-DETACH-PROOF T)
(TOGGLE G0221 DETACH-LIST-IMPLIES T)
(DEFN RT-EXPAN-PROOF (A B PF) (COMMUT-PROOF B A (EXPAN-PROOF B A PF)))
(PROVE-LEMMA RT-EXPAN-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF A)
                          (FORMULA B T 0)
                          (EQUAL CONCL (F-OR A B)))
                     (PROVES (RT-EXPAN-PROOF A B PF) CONCL)))
(TOGGLE G0227 RT-EXPAN-PROOF T)
;Takes list of formulas and returns disjunction.
(DEFN MAKE-DISJUNCT
     (FLIST)
     (IF (NLISTP FLIST)
         NIL
         (IF (NLISTP (CDR FLIST)) (CAR FLIST) (F-OR (CAR FLIST) (MAKE-DISJUNCT (CDR FLIST))))))
(DEFN M1-PROOF
     (EXP FLIST PF)
     (IF (NLISTP FLIST)
         NIL
         (IF (NLISTP (CDR FLIST))
             PF
             (IF (EQUAL EXP (CAR FLIST))
                 (RT-EXPAN-PROOF (CAR FLIST) (MAKE-DISJUNCT (CDR FLIST)) PF)
                 (EXPAN-PROOF (CAR FLIST)
                              (MAKE-DISJUNCT (CDR FLIST))
                              (M1-PROOF EXP (CDR FLIST) PF))))))
(PROVE-LEMMA M1-PROOF-PROVES1
            (REWRITE)
            (IMPLIES (AND (FORMULA (MAKE-DISJUNCT FLIST) T 0)
                          (MEMBER EXP FLIST)
                          (PROVES PF EXP))
                     (PROVES (M1-PROOF EXP FLIST PF) (MAKE-DISJUNCT FLIST)))
            ((DISABLE FORMULA)))
(TOGGLE G0228 M1-PROOF T)
(DEFN RT-ASSOC-PROOF
     (A B C PF)
     (COMMUT-PROOF (F-OR B C)
                   A
                   (ASSOC-PROOF B
                                C
                                A
                                (COMMUT-PROOF (F-OR C A)
                                              B
                                              (ASSOC-PROOF C
                                                           A
                                                           B
                                                           (COMMUT-PROOF (F-OR A B) C PF))))))
(PROVE-LEMMA RT-ASSOC-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF (F-OR (F-OR A B) C))
                          (FORMULA A T 0)
                          (FORMULA B T 0)
                          (FORMULA C T 0)
                          (EQUAL CONCL (F-OR A (F-OR B C))))
                     (PROVES (RT-ASSOC-PROOF A B C PF) CONCL)))
(TOGGLE G0231 RT-ASSOC-PROOF T)
(DEFN INSERT-PROOF
     (A B C PF)
     (COMMUT-PROOF (F-OR A C)
                   B
                   (ASSOC-PROOF A C B (EXPAN-PROOF A (F-OR C B) (COMMUT-PROOF B C PF)))))
(PROVE-LEMMA INSERT-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF (F-OR B C))
                          (FORMULA A T 0)
                          (FORMULA B T 0)
                          (FORMULA C T 0)
                          (EQUAL CONCL (F-OR B (F-OR A C))))
                     (PROVES (INSERT-PROOF A B C PF) CONCL)))
(TOGGLE G0232 INSERT-PROOF T)
(DEFN M2-PROOF-STEP
     (EXP1 EXP2 FLIST PF)
     (IF (NLISTP FLIST)
         NIL
         (IF (NLISTP (CDR FLIST))
             (IF (EQUAL EXP2 (CAR FLIST)) PF NIL)
             (IF (EQUAL EXP2 (CAR FLIST))
                 (RT-ASSOC-PROOF EXP1
                                 EXP2
                                 (MAKE-DISJUNCT (CDR FLIST))
                                 (RT-EXPAN-PROOF (F-OR EXP1 EXP2)
                                                 (MAKE-DISJUNCT (CDR FLIST))
                                                 PF))
                 (INSERT-PROOF (CAR FLIST)
                               EXP1
                               (MAKE-DISJUNCT (CDR FLIST))
                               (M2-PROOF-STEP EXP1 EXP2 (CDR FLIST) PF))))))
(PROVE-LEMMA M2-PROOF-STEP-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA (MAKE-DISJUNCT FLIST) T 0)
                          (MEMBER EXP2 FLIST)
                          (FORMULA EXP1 T 0)
                          (FORMULA EXP2 T 0)
                          (PROVES PF (F-OR EXP1 EXP2)))
                     (PROVES (M2-PROOF-STEP EXP1 EXP2 FLIST PF)
                             (F-OR EXP1 (MAKE-DISJUNCT FLIST))
                            ))
            ((DISABLE FORMULA)))
(PROVE-LEMMA M2-PROOF-STEP-PROVES1
            (REWRITE)
            (IMPLIES (AND (FORMULA (MAKE-DISJUNCT FLIST) T 0)
                          (MEMBER EXP2 FLIST)
                          (FORMULA EXP1 T 0)
                          (FORMULA EXP2 T 0)
                          (PROVES PF (F-OR EXP1 EXP2))
                          (EQUAL CONCL (F-OR EXP1 (MAKE-DISJUNCT FLIST))))
                     (PROVES (M2-PROOF-STEP EXP1 EXP2 FLIST PF) CONCL))
            ((USE (M2-PROOF-STEP-PROVES))))
(TOGGLE G0233 M2-PROOF-STEP T)
(TOGGLE G0234 M2-PROOF-STEP-PROVES T)
(DEFN M2-PROOF
     (EXP1 EXP2 FLIST PF)
     (IF (NLISTP FLIST)
         NIL
         (IF (EQUAL EXP1 EXP2)
             (M1-PROOF EXP1 FLIST (CONTRAC-PROOF EXP1 PF))
             (IF (EQUAL EXP1 (CAR FLIST))
                 (M2-PROOF-STEP EXP1 EXP2 (CDR FLIST) PF)
                 (IF (EQUAL EXP2 (CAR FLIST))
                     (M2-PROOF-STEP EXP2 EXP1 (CDR FLIST) (COMMUT-PROOF EXP1 EXP2 PF))
                     (EXPAN-PROOF (CAR FLIST)
                                  (MAKE-DISJUNCT (CDR FLIST))
                                  (M2-PROOF EXP1 EXP2 (CDR FLIST) PF)))))))
(PROVE-LEMMA M1-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA (MAKE-DISJUNCT FLIST) T 0)
                          (MEMBER EXP FLIST)
                          (PROVES PF EXP)
                          (EQUAL CONCL (MAKE-DISJUNCT FLIST)))
                     (PROVES (M1-PROOF EXP FLIST PF) CONCL))
            ((USE (M1-PROOF-PROVES1))))
(PROVE-LEMMA M2-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA (MAKE-DISJUNCT FLIST) T 0)
                          (FORMULA EXP1 T 0)
                          (FORMULA EXP2 T 0)
                          (MEMBER EXP1 FLIST)
                          (MEMBER EXP2 FLIST)
                          (PROVES PF (F-OR EXP1 EXP2)))
                     (PROVES (M2-PROOF EXP1 EXP2 FLIST PF) (MAKE-DISJUNCT FLIST)))
            ((DISABLE FORMULA)))
(PROVE-LEMMA M2-PROOF-PROVES1
            (REWRITE)
            (IMPLIES (AND (FORMULA (MAKE-DISJUNCT FLIST) T 0)
                          (FORMULA EXP1 T 0)
                          (FORMULA EXP2 T 0)
                          (MEMBER EXP1 FLIST)
                          (MEMBER EXP2 FLIST)
                          (PROVES PF (F-OR EXP1 EXP2))
                          (EQUAL CONCL (MAKE-DISJUNCT FLIST)))
                     (PROVES (M2-PROOF EXP1 EXP2 FLIST PF) CONCL))
            ((USE (M2-PROOF-PROVES))))
(TOGGLE G0235 M2-PROOF T)
(TOGGLE G0236 M2-PROOF-PROVES T)
(DEFN
M3-PROOF
(EXP1 EXP2 FLIST2 PF)
(CONTRAC-PROOF
 (MAKE-DISJUNCT FLIST2)
 (CONTRAC-PROOF
  (F-OR (MAKE-DISJUNCT FLIST2) (MAKE-DISJUNCT FLIST2))
  (M2-PROOF
   (F-OR (MAKE-DISJUNCT FLIST2) (MAKE-DISJUNCT FLIST2))
   EXP1
   (CONS (F-OR (MAKE-DISJUNCT FLIST2) (MAKE-DISJUNCT FLIST2))
         (CONS (MAKE-DISJUNCT FLIST2) FLIST2))
   (ASSOC-PROOF (MAKE-DISJUNCT FLIST2)
                (MAKE-DISJUNCT FLIST2)
                EXP1
                (COMMUT-PROOF (F-OR (MAKE-DISJUNCT FLIST2) EXP1)
                              (MAKE-DISJUNCT FLIST2)
                              (M2-PROOF (F-OR (MAKE-DISJUNCT FLIST2) EXP1)
                                        EXP2
                                        (CONS (F-OR (MAKE-DISJUNCT FLIST2) EXP1) FLIST2)
                                        (ASSOC-PROOF (MAKE-DISJUNCT FLIST2)
                                                     EXP1
                                                     EXP2
                                                     (COMMUT-PROOF (F-OR EXP1 EXP2)
                                                                   (MAKE-DISJUNCT FLIST2)
                                                                   PF)))))))))
(DEFN M-PROOF
     (FLIST1 FLIST2 PF)
     (IF (NLISTP FLIST1)
         NIL
         (IF (NLISTP (CDR FLIST1))
             (M1-PROOF (CAR FLIST1) FLIST2 PF)
             (IF (NLISTP (CDDR FLIST1))
                 (M2-PROOF (CAR FLIST1) (CADR FLIST1) FLIST2 PF)
                 (M3-PROOF (CAR FLIST1)
                           (CADR FLIST1)
                           FLIST2
                           (M-PROOF (CONS (F-OR (CAR FLIST1) (CADR FLIST1)) (CDDR FLIST1))
                                    (CONS (F-OR (CAR FLIST1) (CADR FLIST1)) FLIST2)
                                    (ASSOC-PROOF (CAR FLIST1)
                                                 (CADR FLIST1)
                                                 (MAKE-DISJUNCT (CDDR FLIST1))
                                                 PF))))))
     ((LESSP (LENGTH FLIST1))))
(PROVE-LEMMA SUBSET-CONS (REWRITE) (IMPLIES (SUBSET X Y) (SUBSET X (CONS Z Y))))
(DEFN FORM-LIST
     (FLIST)
     (IF (LISTP FLIST)
         (AND (FORMULA (CAR FLIST) T 0)
              (FORM-LIST (CDR FLIST)))
         T))
(PROVE-LEMMA FORMLIST-FORMULA-MAKE-DISJ
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (LISTP FLIST))
                     (FORMULA (MAKE-DISJUNCT FLIST) T 0))
            ((DISABLE FORMULA)))
(PROVE-LEMMA M3-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA EXP1 T 0)
                          (FORMULA EXP2 T 0)
                          (FORM-LIST FLIST2)
                          (PROVES PF (MAKE-DISJUNCT (CONS (F-OR EXP1 EXP2) FLIST2)))
                          (MEMBER EXP1 FLIST2)
                          (MEMBER EXP2 FLIST2))
                     (PROVES (M3-PROOF EXP1 EXP2 FLIST2 PF) (MAKE-DISJUNCT FLIST2))))
(TOGGLE G0222 M3-PROOF T)
(PROVE-LEMMA M3-PROOF-PROVES1
            (REWRITE)
            (IMPLIES (AND (FORMULA EXP1 T 0)
                          (FORMULA EXP2 T 0)
                          (FORM-LIST FLIST2)
                          (PROVES PF (MAKE-DISJUNCT (CONS (F-OR EXP1 EXP2) FLIST2)))
                          (MEMBER EXP1 FLIST2)
                          (MEMBER EXP2 FLIST2)
                          (EQUAL CONCL (MAKE-DISJUNCT FLIST2)))
                     (PROVES (M3-PROOF EXP1 EXP2 FLIST2 PF) CONCL))
            ((USE (M3-PROOF-PROVES))))
(TOGGLE G0229 M3-PROOF-PROVES T)
;The subset lemma
(PROVE-LEMMA M-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST1)
                          (LISTP FLIST1)
                          (FORM-LIST FLIST2)
                          (LISTP FLIST2)
                          (SUBSET FLIST1 FLIST2)
                          (PROVES PF (MAKE-DISJUNCT FLIST1)))
                     (PROVES (M-PROOF FLIST1 FLIST2 PF) (MAKE-DISJUNCT FLIST2)))
            ((INDUCT (M-PROOF FLIST1 FLIST2 PF))))
(TOGGLE G0247 M-PROOF T)
(PROVE-LEMMA M-PROOF-PROVES1
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST1)
                          (FORM-LIST FLIST2)
                          (SUBSET FLIST1 FLIST2)
                          (PROVES PF (MAKE-DISJUNCT FLIST1))
                          (EQUAL CONCL (MAKE-DISJUNCT FLIST2)))
                     (PROVES (M-PROOF FLIST1 FLIST2 PF) CONCL))
            ((USE (M-PROOF-PROVES))))
;Disjunctions.
(DEFN OR-TYPE (EXP) (EQUAL EXP (F-OR (CADR EXP) (CADDR EXP))))
;Negation of disjunctions.
(DEFN NOR-TYPE (EXP) (EQUAL EXP (F-NOT (F-OR (CADADR EXP) (CADDADR EXP)))))
(TOGGLE G0250 ATOMP T)
;Elementary and negation of elementary formulas
(DEFN ELEM-FORM
     (EXP)
     (OR (ATOMP EXP)
         (EQUAL EXP (FORSOME (CADR EXP) (CADDR EXP)))))
(DEFN NEG-ELEM-FORM
     (EXP)
     (AND (EQUAL EXP (F-NOT (CADR EXP)))
          (ELEM-FORM (ARG1 EXP))))
(DEFN PROP-ATOMP
     (EXP)
     (OR (ELEM-FORM EXP)
         (NEG-ELEM-FORM EXP)))
;Double-negations
(DEFN DBLE-NEG-TYPE (EXP) (EQUAL EXP (F-NOT (F-NOT (CADADR EXP)))))
(TOGGLE G0251 ATOMP NIL)
(PROVE-LEMMA DBLE-NEG-NOT-PROP-ATOMP
            (REWRITE)
            (IMPLIES (DBLE-NEG-TYPE EXP) (NOT (PROP-ATOMP EXP))))
(PROVE-LEMMA OR-TYPE-NOT-PROP-ATOMP (REWRITE) (IMPLIES (OR-TYPE EXP) (NOT (PROP-ATOMP EXP))))
(PROVE-LEMMA NOR-TYPE-NOT-PROP-ATOMP (REWRITE) (IMPLIES (NOR-TYPE EXP) (NOT (PROP-ATOMP EXP))))
(DEFN LIST-COUNT
     (LIST)
     (IF (NLISTP LIST) 0 (PLUS (ADD1 (COUNT (CAR LIST))) (LIST-COUNT (CDR LIST)))))
(DEFN NEG-LIST
     (EXP LIST)
     (IF (NLISTP LIST)
         F
         (OR (NEG EXP (CAR LIST))
             (NEG-LIST EXP (CDR LIST)))))
(PROVE-LEMMA LESSP-LIST-COUNT
            (REWRITE)
            (IMPLIES (LISTP FLIST) (LESSP (LIST-COUNT (CDR FLIST)) (LIST-COUNT FLIST))))
(PROVE-LEMMA OR-TYPE-LIST-COUNT
            (REWRITE)
            (IMPLIES (AND (OR-TYPE (CAR FLIST))
                          (LISTP FLIST))
                     (LESSP (LIST-COUNT (CONS (CADAR FLIST) (CONS (CADDAR FLIST) (CDR FLIST))))
                            (LIST-COUNT FLIST))))
(PROVE-LEMMA NOR-TYPE-LIST-COUNT1
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST)
                          (NOR-TYPE (CAR FLIST)))
                     (LESSP (LIST-COUNT (CONS (LIST 'NOT (CADADAR FLIST)) (CDR FLIST)))
                            (LIST-COUNT FLIST))))
(PROVE-LEMMA NOR-TYPE-LIST-COUNT2
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST)
                          (NOR-TYPE (CAR FLIST)))
                     (LESSP (LIST-COUNT (CONS (LIST 'NOT (CADDADAR FLIST)) (CDR FLIST)))
                            (LIST-COUNT FLIST))))
(PROVE-LEMMA DBLE-NEG-LIST-COUNT
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST)
                          (DBLE-NEG-TYPE (CAR FLIST)))
                     (LESSP (LIST-COUNT (CONS (CADADAR FLIST) (CDR FLIST))) (LIST-COUNT FLIST))))
(TOGGLE G0230 PROP-ATOMP T)
(TOGGLE G0237 OR-TYPE T)
(TOGGLE G0238 NOR-TYPE T)
(TOGGLE G0239 DBLE-NEG-TYPE T)
(TOGGLE G0240 LIST-COUNT T)
;The tautology-checker.
(DEFN TAUTOLOGYP1
     (FLIST AUXLIST)
     (IF (NLISTP FLIST)
         F
         (IF (PROP-ATOMP (CAR FLIST))
             (OR (NEG-LIST (CAR FLIST) AUXLIST)
                 (TAUTOLOGYP1 (CDR FLIST) (CONS (CAR FLIST) AUXLIST)))
             (IF (OR-TYPE (CAR FLIST))
                 (TAUTOLOGYP1 (CONS (ARG1 (CAR FLIST)) (CONS (ARG2 (CAR FLIST)) (CDR FLIST))) AUXLIST)
                 (IF (NOR-TYPE (CAR FLIST))
                     (AND (TAUTOLOGYP1 (CONS (F-NOT (ARG1 (ARG1 (CAR FLIST)))) (CDR FLIST)) AUXLIST)
                          (TAUTOLOGYP1 (CONS (F-NOT (ARG2 (ARG1 (CAR FLIST)))) (CDR FLIST)) AUXLIST))
                     (IF (DBLE-NEG-TYPE (CAR FLIST))
                         (TAUTOLOGYP1 (CONS (ARG1 (ARG1 (CAR FLIST))) (CDR FLIST)) AUXLIST)
                         F)))))
     ((LESSP (LIST-COUNT FLIST))))
(PROVE-LEMMA FORM-LIST-APPEND
            (REWRITE)
            (IMPLIES (AND (FORM-LIST X)
                          (FORM-LIST Y))
                     (FORM-LIST (APPEND X Y)))
            ((INDUCT (APPEND X Y)) (DISABLE FORMULA)))
(DEFN NEG-PROOF
     (EXP1 EXP2)
     (IF (EQUAL EXP1 (F-NOT EXP2))
         (PROP-AXIOM-PROOF EXP2)
         (COMMUT-PROOF EXP2 EXP1 (PROP-AXIOM-PROOF EXP1))))
(PROVE-LEMMA NEG-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA EXP1 T 0)
                          (FORMULA EXP2 T 0)
                          (NEG EXP1 EXP2)
                          (EQUAL CONCL (F-OR EXP1 EXP2)))
                     (PROVES (NEG-PROOF EXP1 EXP2) CONCL)))
(TOGGLE G0245 NEG-PROOF T)
(PROVE-LEMMA NEG-LIST-REDUC
            (REWRITE)
            (EQUAL (NEG-LIST EXP FLIST)
                   (OR (MEMBER (F-NOT EXP) FLIST)
                       (AND (EQUAL EXP (F-NOT (CADR EXP)))
                            (MEMBER (CADR EXP) FLIST)))))
(DEFN NEG-LIST-PROOF
     (EXP FLIST)
     (IF (MEMBER (F-NOT EXP) FLIST)
         (M2-PROOF EXP (F-NOT EXP) (CONS EXP FLIST) (NEG-PROOF EXP (F-NOT EXP)))
         (M2-PROOF EXP (CADR EXP) (CONS EXP FLIST) (NEG-PROOF EXP (CADR EXP)))))
(PROVE-LEMMA NEG-LIST-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA EXP T 0)
                          (FORM-LIST FLIST)
                          (NEG-LIST EXP FLIST)
                          (EQUAL CONCL (MAKE-DISJUNCT (CONS EXP FLIST))))
                     (PROVES (NEG-LIST-PROOF EXP FLIST) CONCL))
            ((DISABLE NEG-LIST)))
(TOGGLE G0256 NEG-LIST-PROOF T)
(PROVE-LEMMA SUBSET-IDENT (REWRITE) (SUBSET X X))
(PROVE-LEMMA SUBSET-CAR (REWRITE) (SUBSET X (CONS Y X)))
(PROVE-LEMMA SUBSET-APPEND (REWRITE) (SUBSET (CONS EXP LIST2) (APPEND (CONS EXP LIST1) LIST2)))
(PROVE-LEMMA NLISTP-NEG-LIST (REWRITE) (IMPLIES (NLISTP LIST) (NOT (NEG-LIST EXP LIST))))
(DEFN PROP-ATOM-PROOF1
     (FLIST1 FLIST2)
     (M-PROOF (CONS (CAR FLIST1) FLIST2)
              (APPEND FLIST1 FLIST2)
              (NEG-LIST-PROOF (CAR FLIST1) FLIST2)))
(PROVE-LEMMA PROP-ATOM-PROOF1-PROVES
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST1)
                          (LISTP FLIST1)
                          (FORM-LIST FLIST2)
                          (NEG-LIST (CAR FLIST1) FLIST2)
                          (EQUAL CONCL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2))))
                     (PROVES (PROP-ATOM-PROOF1 FLIST1 FLIST2) CONCL))
            ((DISABLE NEG-LIST-REDUC) (USE (SUBSET-APPEND (EXP (CAR FLIST1))
                                                          (LIST1 (CDR FLIST1))
                                                          (LIST2 FLIST2)))))
(TOGGLE G0259 PROP-ATOM-PROOF1 T)
(PROVE-LEMMA SUBSET-APPEND-CAR
            (REWRITE)
            (SUBSET (APPEND LIST1 (CONS EXP LIST2)) (APPEND (CONS EXP LIST1) LIST2)))
(PROVE-LEMMA FORM-LIST-APPEND-CAR
            (REWRITE)
            (IMPLIES (AND (FORM-LIST (CONS EXP LIST1))
                          (FORM-LIST LIST2))
                     (FORM-LIST (APPEND LIST1 (CONS EXP LIST2)))))
(DEFN PROP-ATOM-PROOF2
     (FLIST1 FLIST2 PF)
     (M-PROOF (APPEND (CDR FLIST1) (CONS (CAR FLIST1) FLIST2)) (APPEND FLIST1 FLIST2) PF))
(PROVE-LEMMA PROP-ATOM-PROOF2-PROVES
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST1)
                          (LISTP FLIST1)
                          (FORM-LIST FLIST2)
                          (PROVES PF
                                  (MAKE-DISJUNCT (APPEND (CDR FLIST1) (CONS (CAR FLIST1) FLIST2)))
                                 )
                          (EQUAL CONCL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2))))
                     (PROVES (PROP-ATOM-PROOF2 FLIST1 FLIST2 PF) CONCL))
            ((USE (SUBSET-APPEND-CAR (LIST1 (CDR FLIST1)) (EXP (CAR FLIST1)) (LIST2 FLIST2)))))
(TOGGLE G0258 PROP-ATOM-PROOF2 T)
(DEFN CANCEL-PROOF
     (A B PF1 PF2)
     (CONTRAC-PROOF B (CUT-PROOF A B B PF2 (RT-EXPAN-PROOF (F-NOT A) B PF1))))
(PROVE-LEMMA CANCEL-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (PROVES PF1 (F-NOT A))
                          (PROVES PF2 (F-OR A B))
                          (FORMULA A T 0)
                          (FORMULA B T 0))
                     (PROVES (CANCEL-PROOF A B PF1 PF2) B)))
(TOGGLE G0255 CANCEL-PROOF T)
(DEFN NLISTP-NOR-TYPE-PROOF
     (A B PF1 PF2)
     (CANCEL-PROOF B
                   (F-NOT (F-OR A B))
                   PF2
                   (CANCEL-PROOF A
                                 (F-OR B (F-NOT (F-OR A B)))
                                 PF1
                                 (M-PROOF (LIST (F-NOT (F-OR A B)) A B)
                                          (LIST A B (F-NOT (F-OR A B)))
                                          (PROP-AXIOM-PROOF (F-OR A B))))))
(PROVE-LEMMA NLISTP-NOR-TYPE-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA A T 0)
                          (FORMULA B T 0)
                          (PROVES PF1 (F-NOT A))
                          (PROVES PF2 (F-NOT B))
                          (EQUAL CONCL (F-NOT (F-OR A B))))
                     (PROVES (NLISTP-NOR-TYPE-PROOF A B PF1 PF2) CONCL)))
(DEFN
LISTP-NOR-TYPE-PROOF
(A B C PF1 PF2)
(M-PROOF
 (LIST (F-NOT (F-OR A B)) C C)
 (LIST (F-NOT (F-OR A B)) C)
 (RT-ASSOC-PROOF (F-NOT (F-OR A B))
                 C
                 C
                 (CUT-PROOF B
                            (F-OR (F-NOT (F-OR A B)) C)
                            C
                            (RT-ASSOC-PROOF B
                                            (F-NOT (F-OR A B))
                                            C
                                            (CUT-PROOF A
                                                       (F-OR B (F-NOT (F-OR A B)))
                                                       C
                                                       (M-PROOF (LIST (F-NOT (F-OR A B)) A B)
                                                                (LIST A B (F-NOT (F-OR A B)))
                                                                (PROP-AXIOM-PROOF (F-OR A B)))
                                                       PF1))
                            PF2))))
(PROVE-LEMMA LISTP-NOR-TYPE-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA A T 0)
                          (FORMULA B T 0)
                          (FORMULA C T 0)
                          (PROVES PF1 (F-OR (F-NOT A) C))
                          (PROVES PF2 (F-OR (F-NOT B) C))
                          (EQUAL CONCL (F-OR (F-NOT (F-OR A B)) C)))
                     (PROVES (LISTP-NOR-TYPE-PROOF A B C PF1 PF2) CONCL)))
(TOGGLE G0242 M-PROOF-PROVES T)
(TOGGLE G0243 NLISTP-NOR-TYPE-PROOF T)
(TOGGLE G0244 LISTP-NOR-TYPE-PROOF T)
(DEFN NOR-TYPE-PROOF
     (A B CLIST PF1 PF2)
     (IF (NLISTP CLIST)
         (NLISTP-NOR-TYPE-PROOF A B PF1 PF2)
         (LISTP-NOR-TYPE-PROOF A B (MAKE-DISJUNCT CLIST) PF1 PF2)))
(TOGGLE G0292 NOR-TYPE NIL)
(PROVE-LEMMA NOR-TYPE-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (NOR-TYPE EXP)
                          (FORMULA EXP T 0)
                          (FORM-LIST CLIST)
                          (PROVES PF1 (MAKE-DISJUNCT (CONS (F-NOT (CADADR EXP)) CLIST)))
                          (PROVES PF2 (MAKE-DISJUNCT (CONS (F-NOT (CADDADR EXP)) CLIST)))
                          (EQUAL CONCL (MAKE-DISJUNCT (CONS EXP CLIST))))
                     (PROVES (NOR-TYPE-PROOF (CADADR EXP) (CADDADR EXP) CLIST PF1 PF2)
                             CONCL
                            )))
(DEFN NLISTP-DBLE-NEG-PROOF
     (A PF)
     (CONTRAC-PROOF (F-NOT (F-NOT A))
                    (CUT-PROOF A
                               (F-NOT (F-NOT A))
                               (F-NOT (F-NOT A))
                               (RT-EXPAN-PROOF A (F-NOT (F-NOT A)) PF)
                               (COMMUT-PROOF (F-NOT (F-NOT A))
                                             (F-NOT A)
                                             (PROP-AXIOM-PROOF (F-NOT A))))))
(TOGGLE G0248 NOR-TYPE-PROOF T)
(PROVE-LEMMA NLISTP-DBLE-NEG-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA A T 0)
                          (PROVES PF A)
                          (EQUAL CONCL (F-NOT (F-NOT A))))
                     (PROVES (NLISTP-DBLE-NEG-PROOF A PF) CONCL)))
(TOGGLE G0249 NLISTP-DBLE-NEG-PROOF T)
(DEFN LISTP-DBLE-NEG-PROOF
     (A C PF)
     (COMMUT-PROOF C
                   (F-NOT (F-NOT A))
                   (CUT-PROOF A
                              C
                              (F-NOT (F-NOT A))
                              PF
                              (COMMUT-PROOF (F-NOT (F-NOT A))
                                            (F-NOT A)
                                            (PROP-AXIOM-PROOF (F-NOT A))))))
(PROVE-LEMMA LISTP-DBLE-NEG-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (FORMULA A T 0)
                          (FORMULA C T 0)
                          (PROVES PF (F-OR A C))
                          (EQUAL CONCL (F-OR (F-NOT (F-NOT A)) C)))
                     (PROVES (LISTP-DBLE-NEG-PROOF A C PF) CONCL)))
(TOGGLE G0203 LISTP-DBLE-NEG-PROOF T)
(DEFN DBLE-NEG-TYPE-PROOF
     (A CLIST PF)
     (IF (NLISTP CLIST)
         (NLISTP-DBLE-NEG-PROOF A PF)
         (LISTP-DBLE-NEG-PROOF A (MAKE-DISJUNCT CLIST) PF)))
(TOGGLE G0252 DBLE-NEG-TYPE NIL)
(PROVE-LEMMA DBLE-NEG-TYPE-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (DBLE-NEG-TYPE EXP)
                          (FORMULA EXP T 0)
                          (FORM-LIST CLIST)
                          (PROVES PF (MAKE-DISJUNCT (CONS (CADADR EXP) CLIST)))
                          (EQUAL CONCL (MAKE-DISJUNCT (CONS EXP CLIST))))
                     (PROVES (DBLE-NEG-TYPE-PROOF (CADADR EXP) CLIST PF) CONCL)))
(DEFN OR-TYPE-PROOF
     (A B CLIST PF)
     (IF (NLISTP CLIST) PF (ASSOC-PROOF A B (MAKE-DISJUNCT CLIST) PF)))
(TOGGLE G0260 OR-TYPE NIL)
(PROVE-LEMMA OR-TYPE-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (OR-TYPE (CAR FLIST1))
                          (FORM-LIST FLIST1)
                          (LISTP FLIST1)
                          (FORM-LIST FLIST2)
                          (PROVES PF
                                  (MAKE-DISJUNCT (APPEND (CONS (CADAR FLIST1)
                                                               (CONS (CADDAR FLIST1)
                                                                     (CDR FLIST1)))
                                                         FLIST2))
                                 )
                          (EQUAL CONCL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2))))
                     (PROVES (OR-TYPE-PROOF (CADAR FLIST1)
                                            (CADDAR FLIST1)
                                            (APPEND (CDR FLIST1) FLIST2)
                                            PF)
                             CONCL
                            )))
(TOGGLE G0271 OR-TYPE-PROOF T)
(PROVE-LEMMA OR-TYPE-FORM-LIST
            (REWRITE)
            (IMPLIES (AND (OR-TYPE (CAR FLIST))
                          (FORM-LIST FLIST)
                          (LISTP FLIST))
                     (FORM-LIST (CONS (CADAR FLIST) (CONS (CADDAR FLIST) (CDR FLIST))))))
(PROVE-LEMMA NOR-TYPE-FORM-LIST
            (REWRITE)
            (IMPLIES (AND (NOR-TYPE (CAR FLIST))
                          (FORM-LIST FLIST)
                          (LISTP FLIST))
                     (FORM-LIST (CONS (LIST 'NOT (CADADAR FLIST)) (CDR FLIST)))))
(PROVE-LEMMA NOR-TYPE-FORM-LIST2
            (REWRITE)
            (IMPLIES (AND (NOR-TYPE (CAR FLIST))
                          (FORM-LIST FLIST)
                          (LISTP FLIST))
                     (FORM-LIST (CONS (LIST 'NOT (CADDADAR FLIST)) (CDR FLIST)))))
(PROVE-LEMMA DBLE-NEG-TYPE-FORM-LIST
            (REWRITE)
            (IMPLIES (AND (DBLE-NEG-TYPE (CAR FLIST))
                          (FORM-LIST FLIST)
                          (LISTP FLIST))
                     (FORM-LIST (CONS (CADADAR FLIST) (CDR FLIST)))))
(TOGGLE G0272 OR-TYPE T)
(TOGGLE G0273 NOR-TYPE T)
(TOGGLE G0274 DBLE-NEG-TYPE T)
(TOGGLE G0254 DBLE-NEG-TYPE-PROOF T)
;The proof-constructor for tautologies.
(DEFN TAUT-PROOF1
     (FLIST AUXLIST)
     (IF (NLISTP FLIST)
         NIL
         (IF (PROP-ATOMP (CAR FLIST))
             (IF (NEG-LIST (CAR FLIST) AUXLIST)
                 (PROP-ATOM-PROOF1 FLIST AUXLIST)
                 (PROP-ATOM-PROOF2 FLIST
                                   AUXLIST
                                   (TAUT-PROOF1 (CDR FLIST) (CONS (CAR FLIST) AUXLIST))))
             (IF (OR-TYPE (CAR FLIST))
                 (OR-TYPE-PROOF (ARG1 (CAR FLIST))
                                (ARG2 (CAR FLIST))
                                (APPEND (CDR FLIST) AUXLIST)
                                (TAUT-PROOF1 (CONS (ARG1 (CAR FLIST))
                                                   (CONS (ARG2 (CAR FLIST)) (CDR FLIST)))
                                             AUXLIST))
                 (IF (NOR-TYPE (CAR FLIST))
                     (NOR-TYPE-PROOF (ARG1 (ARG1 (CAR FLIST)))
                                     (ARG2 (ARG1 (CAR FLIST)))
                                     (APPEND (CDR FLIST) AUXLIST)
                                     (TAUT-PROOF1 (CONS (F-NOT (ARG1 (ARG1 (CAR FLIST)))) (CDR FLIST))
                                                  AUXLIST)
                                     (TAUT-PROOF1 (CONS (F-NOT (ARG2 (ARG1 (CAR FLIST)))) (CDR FLIST))
                                                  AUXLIST))
                     (IF (DBLE-NEG-TYPE (CAR FLIST))
                         (DBLE-NEG-TYPE-PROOF (ARG1 (ARG1 (CAR FLIST)))
                                              (APPEND (CDR FLIST) AUXLIST)
                                              (TAUT-PROOF1 (CONS (ARG1 (ARG1 (CAR FLIST))) (CDR FLIST))
                                                           AUXLIST))
                         NIL)))))
     ((LESSP (LIST-COUNT FLIST))))
;Every tautology has a proof (when AUXLIST is NIL)
(PROVE-LEMMA TAUT-THM1
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (FORM-LIST AUXLIST)
                          (TAUTOLOGYP1 FLIST AUXLIST))
                     (PROVES (TAUT-PROOF1 FLIST AUXLIST)
                             (MAKE-DISJUNCT (APPEND FLIST AUXLIST))
                            ))
            ((DISABLE NEG-LIST-REDUC FORMULA) (INDUCT (TAUTOLOGYP1 FLIST AUXLIST))))
(TOGGLE G0275 TAUT-PROOF1 T)
(PROVE-LEMMA TAUT-THM2
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (FORM-LIST AUXLIST)
                          (TAUTOLOGYP1 FLIST AUXLIST)
                          (EQUAL CONCL (MAKE-DISJUNCT (APPEND FLIST AUXLIST))))
                     (PROVES (TAUT-PROOF1 FLIST AUXLIST) CONCL))
            ((USE (TAUT-THM1 (CONCL (MAKE-DISJUNCT (APPEND FLIST AUXLIST)))))))
(PROVE-LEMMA LISTP-ELEM-FORM (REWRITE) (IMPLIES (NLISTP EXP) (NOT (ELEM-FORM EXP))))
;Truth value evaluator.
(DEFN EVAL
     (EXP ALIST)
     (IF (NLISTP EXP)
         F
         (IF (ELEM-FORM EXP)
             (MEMBER EXP ALIST)
             (IF (EQUAL (CAR EXP) 'NOT)
                 (NOT (EVAL (CADR EXP) ALIST))
                 (IF (EQUAL (CAR EXP) 'OR)
                     (OR (EVAL (CADR EXP) ALIST)
                         (EVAL (CADDR EXP) ALIST))
                     F)))))
(PROVE-LEMMA ELEM-FORM-EVAL
            (REWRITE)
            (IMPLIES (ELEM-FORM EXP) (EQUAL (EVAL EXP ALIST) (MEMBER EXP ALIST))))
(PROVE-LEMMA NLISTP-EVAL (REWRITE) (IMPLIES (NLISTP EXP) (NOT (EVAL EXP ALIST))))
(PROVE-LEMMA NOT-EVAL
            (REWRITE)
            (IMPLIES (AND (LISTP EXP)
                          (EQUAL (CAR EXP) 'NOT))
                     (EQUAL (EVAL EXP ALIST) (NOT (EVAL (CADR EXP) ALIST)))))
(PROVE-LEMMA OR-EVAL
            (REWRITE)
            (IMPLIES (AND (LISTP EXP)
                          (EQUAL (CAR EXP) 'OR))
                     (EQUAL (EVAL EXP ALIST)
                            (OR (EVAL (CADR EXP) ALIST)
                                (EVAL (CADDR EXP) ALIST)))))
(PROVE-LEMMA MEMBER-EVAL (REWRITE)
            (IMPLIES (AND (MEMBER EXP FLIST)
                          (EVAL EXP ALIST))
                     (EVAL (MAKE-DISJUNCT FLIST) ALIST)))
(PROVE-LEMMA EVAL-ELEM-FORM
            (REWRITE)
            (IMPLIES (AND (ELEM-FORM EXP)
                          (MEMBER EXP LIST)
                          (MEMBER EXP ALIST)
                          (EQUAL CONCL (MAKE-DISJUNCT LIST)))
                     (EVAL CONCL ALIST))
            ((INDUCT (MEMBER EXP LIST)) (DISABLE EVAL ELEM-FORM)))
(TOGGLE G0278 OR-TYPE NIL)
(TOGGLE G0279 NOR-TYPE NIL)
(TOGGLE G0280 DBLE-NEG-TYPE NIL)
(TOGGLE G0281 PROP-ATOMP NIL)
(PROVE-LEMMA MEMBER-APPEND
            (REWRITE)
            (EQUAL (MEMBER EXP (APPEND FLIST1 FLIST2))
                   (OR (MEMBER EXP FLIST1)
                       (MEMBER EXP FLIST2))))
(PROVE-LEMMA EVAL-NEG-ELEM-FORM
            (REWRITE)
            (IMPLIES (AND (MEMBER EXP LIST)
                          (MEMBER (F-NOT EXP) LIST)
                          (EQUAL CONCL (MAKE-DISJUNCT LIST)))
                     (EVAL CONCL ALIST))
            ((DISABLE ELEM-FORM EVAL)))
(PROVE-LEMMA EVAL-MAKE-DISJUNCT (REWRITE)
            (EQUAL (EVAL (MAKE-DISJUNCT (APPEND LIST1 LIST2)) ALIST)
                   (OR (EVAL (MAKE-DISJUNCT LIST1) ALIST)
                       (EVAL (MAKE-DISJUNCT LIST2) ALIST))))
(PROVE-LEMMA NEG-LIST-EVAL
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST1)
                          (NEG-LIST (CAR FLIST1) FLIST2)
                          (EQUAL CONCL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2))))
                     (EVAL CONCL ALIST)))
(PROVE-LEMMA EVAL-PROP-ATOMP
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST1)
                          (EVAL (MAKE-DISJUNCT (APPEND (CDR FLIST1) (CONS (CAR FLIST1) FLIST2)))
                                ALIST))
                     (EVAL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2)) ALIST))
            ((INDUCT (APPEND FLIST FLIST2))))
(TOGGLE G1253 EVAL T)
(PROVE-LEMMA EVAL-OR-TYPE
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST1)
                          (OR-TYPE (CAR FLIST1)))
                     (EQUAL (EVAL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2)) ALIST)
                            (EVAL (MAKE-DISJUNCT (APPEND (CONS (CADAR FLIST1)
                                                               (CONS (CADDAR FLIST1)
                                                                     (CDR FLIST1)))
                                                         FLIST2))
                                  ALIST))))
(PROVE-LEMMA EVAL-NOR-TYPE
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST1)
                          (NOR-TYPE (CAR FLIST1)))
                     (EQUAL (EVAL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2)) ALIST)
                            (AND (EVAL (MAKE-DISJUNCT (APPEND (CONS (F-NOT (CADADAR FLIST1))
                                                                    (CDR FLIST1))
                                                              FLIST2))
                                       ALIST)
                                 (EVAL (MAKE-DISJUNCT (APPEND (CONS (F-NOT (CADDADAR FLIST1))
                                                                    (CDR FLIST1))
                                                              FLIST2))
                                       ALIST)))))
(PROVE-LEMMA EVAL-DBLE-NEG-TYPE
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST1)
                          (DBLE-NEG-TYPE (CAR FLIST1)))
                     (EQUAL (EVAL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2)) ALIST)
                            (EVAL (MAKE-DISJUNCT (APPEND (CONS (CADADAR FLIST1) (CDR FLIST1))
                                                         FLIST2))
                                  ALIST))))
;All tautologies are logically-true.
(PROVE-LEMMA TAUT-EVAL
            (REWRITE)
            (IMPLIES (TAUTOLOGYP1 FLIST AUXLIST)
                     (EVAL (MAKE-DISJUNCT (APPEND FLIST AUXLIST)) ALIST))
            ((DISABLE EVAL EVAL-MAKE-DISJUNCT
                      ELEM-FORM
                      PROP-ATOMP
                      OR-TYPE
                      NOR-TYPE
                      DBLE-NEG-TYPE
                      APPEND
                      NEG-LIST-REDUC)
             (INDUCT (TAUTOLOGYP1 FLIST AUXLIST))))
(PROVE-LEMMA NOT-EVAL-PROP-ATOMP
            (REWRITE)
            (IMPLIES (AND (LISTP FLIST1)
                          (NOT (EVAL (MAKE-DISJUNCT (APPEND (CDR FLIST1)
                                                            (CONS (CAR FLIST1) FLIST2)))
                                     ALIST)))
                     (NOT (EVAL (MAKE-DISJUNCT (APPEND FLIST1 FLIST2)) ALIST)))
            ((INDUCT (APPEND FLIST1 FLIST2))))
(PROVE-LEMMA PROP-ATOMP-REDUC
            (REWRITE)
            (EQUAL (PROP-ATOMP EXP)
                   (OR (ELEM-FORM EXP)
                       (AND (EQUAL EXP (F-NOT (CADR EXP)))
                            (ELEM-FORM (CADR EXP)))))
            ((DISABLE ELEM-FORM)))
(TOGGLE G0263 ELEM-FORM T)
(TOGGLE G0264 PROP-ATOMP T)
(DEFN PROP-ATOMP-LIST
     (LIST)
     (IF (NLISTP LIST)
         T
         (AND (PROP-ATOMP (CAR LIST))
              (PROP-ATOMP-LIST (CDR LIST)))))
(DEFN FALSIFY
     (LIST)
     (IF (NLISTP LIST)
         NIL
         (IF (EQUAL (CAR LIST) (F-NOT (CADAR LIST)))
             (CONS (CADAR LIST) (FALSIFY (CDR LIST)))
             (FALSIFY (CDR LIST)))))
(PROVE-LEMMA FALSIFY-STEP
            (REWRITE)
            (IMPLIES (NOT (MEMBER (F-NOT EXP) AUXLIST)) (NOT (MEMBER EXP (FALSIFY AUXLIST)))))
(PROVE-LEMMA PROP-ATOMP-AUXLIST
            (REWRITE)
            (IMPLIES (AND (PROP-ATOMP EXP)
                          (NOT (NEG-LIST EXP AUXLIST))
                          (PROP-ATOMP-LIST AUXLIST))
                     (NOT (EVAL EXP (FALSIFY (CONS EXP AUXLIST)))))
            ((DISABLE FORMULA ELEM-FORM)))
(PROVE-LEMMA
PROP-ATOMP-AUXLIST2
(REWRITE)
(IMPLIES (AND (NOT (NEG-LIST EXP AUXLIST))
              (PROP-ATOMP-LIST AUXLIST)
              (PROP-ATOMP EXP)
              (NOT (EVAL (MAKE-DISJUNCT AUXLIST) (FALSIFY ALIST))))
         (NOT (EVAL (MAKE-DISJUNCT AUXLIST) (FALSIFY (CONS EXP ALIST)))))
((DISABLE FORMULA-NOT-REDUC ELEM-FORM FORMULA PROP-ATOMP NEG-LIST-REDUC)
 (INDUCT (MAKE-DISJUNCT AUXLIST))))
(PROVE-LEMMA PROP-ATOMP-FALSIFY
            (REWRITE)
            (IMPLIES (AND (PROP-ATOMP EXP)
                          (NOT (NEG-LIST EXP AUXLIST))
                          (PROP-ATOMP-LIST AUXLIST)
                          (NOT (EVAL (MAKE-DISJUNCT AUXLIST) (FALSIFY AUXLIST))))
                     (NOT (EVAL (MAKE-DISJUNCT (CONS EXP AUXLIST)) (FALSIFY (CONS EXP AUXLIST)))))
            ((DISABLE ELEM-FORM
                      PROP-ATOMP
                      PROP-ATOMP-REDUC
                      PROP-ATOMP-LIST
                      NEG-LIST-REDUC
                      NEG-LIST
                      FORMULA
                      FALSIFY)
             ))
(TOGGLE G0268 PROP-ATOMP NIL)
(TOGGLE G0269 ELEM-FORM NIL)
(TOGGLE G0204 ATOMP T)
(PROVE-LEMMA FORMULA-CASES1
            NIL
            (IMPLIES (FORMULA EXP T 0)
                     (OR (PROP-ATOMP EXP)
                         (OR-TYPE EXP)
                         (NOR-TYPE EXP)
                         (DBLE-NEG-TYPE EXP))))
(TOGGLE G0205 ATOMP NIL)
(TOGGLE G0296 PROP-ATOMP T)
(TOGGLE G0297 OR-TYPE T)
(TOGGLE G0298 NOR-TYPE T)
(TOGGLE G0299 DBLE-NEG-TYPE T)
(PROVE-LEMMA FORMULA-CASES
            (REWRITE)
            (IMPLIES (AND (NOT (DBLE-NEG-TYPE EXP))
                          (NOT (NOR-TYPE EXP))
                          (NOT (OR-TYPE EXP))
                          (NOT (PROP-ATOMP EXP)))
                     (NOT (FORMULA EXP T 0)))
            ((DISABLE FORMULA PROP-ATOMP-REDUC) (USE (FORMULA-CASES1))))
(DEFN FALSIFY-TAUT
     (FLIST AUXLIST)
     (IF (NLISTP FLIST)
         (FALSIFY AUXLIST)
         (IF (PROP-ATOMP (CAR FLIST))
             (IF (NEG-LIST (CAR FLIST) AUXLIST)
                 F
                 (FALSIFY-TAUT (CDR FLIST) (CONS (CAR FLIST) AUXLIST)))
             (IF (OR-TYPE (CAR FLIST))
                 (FALSIFY-TAUT (CONS (CADAR FLIST) (CONS (CADDAR FLIST) (CDR FLIST))) AUXLIST)
                 (IF (NOR-TYPE (CAR FLIST))
                     (IF (FALSIFY-TAUT (CONS (F-NOT (CADDADAR FLIST)) (CDR FLIST)) AUXLIST)
                         (FALSIFY-TAUT (CONS (F-NOT (CADDADAR FLIST)) (CDR FLIST)) AUXLIST)
                         (FALSIFY-TAUT (CONS (F-NOT (CADADAR FLIST)) (CDR FLIST)) AUXLIST))
                     (IF (DBLE-NEG-TYPE (CAR FLIST))
                         (FALSIFY-TAUT (CONS (CADADAR FLIST) (CDR FLIST)) AUXLIST)
                         NIL)))))
     ((LESSP (LIST-COUNT FLIST))))
(PROVE-LEMMA APPEND-NLISTP (REWRITE) (IMPLIES (NLISTP X) (EQUAL (APPEND X Y) Y)))
(PROVE-LEMMA NOT-FALSIFY-TAUT
            (REWRITE)
            (EQUAL (TAUTOLOGYP1 FLIST AUXLIST) (NOT (FALSIFY-TAUT FLIST AUXLIST)))
            ((INDUCT (TAUTOLOGYP1 FLIST AUXLIST)) (DISABLE NEG-LIST
                                                           NEG-LIST-REDUC
                                                           FORMULA
                                                           PROP-ATOMP-REDUC)))
;Non-tautologies are falsifiable.
(PROVE-LEMMA NOT-TAUT-FALSE
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (PROP-ATOMP-LIST AUXLIST)
                          (NOT (EVAL (MAKE-DISJUNCT AUXLIST) (FALSIFY AUXLIST)))
                          (NOT (TAUTOLOGYP1 FLIST AUXLIST)))
                     (NOT (EVAL (MAKE-DISJUNCT (APPEND FLIST AUXLIST))
                                (FALSIFY-TAUT FLIST AUXLIST))))
            ((INDUCT (FALSIFY-TAUT FLIST AUXLIST))
             (DISABLE NEG-LIST EVAL-MAKE-DISJUNCT        
                      NEG-LIST-REDUC
                      PROP-ATOMP-REDUC
                      FORMULA
                      FALSIFY
                      APPEND
                      NOR-TYPE)))
(DEFN TAUTOLOGYP (FLIST) (TAUTOLOGYP1 FLIST NIL))
(DEFN TAUT-PROOF (FLIST) (TAUT-PROOF1 FLIST NIL))
(TOGGLE G0300 APPEND NIL)
(PROVE-LEMMA FORM-LIST-APPEND-NIL
            (REWRITE)
            (EQUAL (MAKE-DISJUNCT (APPEND FLIST NIL)) (MAKE-DISJUNCT FLIST)))
(PROVE-LEMMA TAUTOLOGY-THEOREM
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (TAUTOLOGYP FLIST)
                          (EQUAL CONCL (MAKE-DISJUNCT FLIST)))
                     (PROVES (TAUT-PROOF FLIST) CONCL))
            ((DISABLE TAUT-PROOF1 TAUTOLOGYP1 FORMULA NOT-FALSIFY-TAUT)))
(PROVE-LEMMA TAUT-EVAL2
            (REWRITE)
            (IMPLIES (AND (TAUTOLOGYP1 FLIST AUXLIST)
                          (EQUAL CONCL (MAKE-DISJUNCT (APPEND FLIST AUXLIST))))
                     (EVAL CONCL ALIST))
            ((DISABLE TAUTOLOGYP1 NOT-FALSIFY-TAUT)))
(PROVE-LEMMA TAUTOLOGIES-ARE-TRUE
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (TAUTOLOGYP FLIST))
                     (EVAL (MAKE-DISJUNCT FLIST) ALIST))
            ((DISABLE FORMULA TAUTOLOGYP1 NOT-FALSIFY-TAUT)))
(PROVE-LEMMA NOT-TAUT-FALSIFY2
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (PROP-ATOMP-LIST AUXLIST)
                          (NOT (EVAL (MAKE-DISJUNCT AUXLIST) (FALSIFY AUXLIST)))
                          (NOT (TAUTOLOGYP1 FLIST AUXLIST))
                          (EQUAL CONCL (MAKE-DISJUNCT (APPEND FLIST AUXLIST))))
                     (NOT (EVAL CONCL (FALSIFY-TAUT FLIST AUXLIST))))
            ((DISABLE TAUTOLOGYP1 NOT-FALSIFY-TAUT FORMULA)))
(PROVE-LEMMA TRUTHS-ARE-TAUTOLOGIES
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (NOT (TAUTOLOGYP FLIST)))
                     (NOT (EVAL (MAKE-DISJUNCT FLIST) (FALSIFY-TAUT FLIST NIL))))
            ((DISABLE TAUTOLOGYP1 NOT-FALSIFY-TAUT FORMULA)))
(TOGGLE G2439 TRUTHS-ARE-TAUTOLOGIES T)
(TOGGLE G2440 NOT-TAUT-FALSIFY2 T)
(TOGGLE G2441 TAUTOLOGIES-ARE-TRUE T)
(TOGGLE G2442 TAUT-EVAL2 T)
(TOGGLE G2443 FORM-LIST-APPEND-NIL T)
(TOGGLE G2444 TAUT-PROOF T)
(TOGGLE G2445 NOT-TAUT-FALSE T)
(TOGGLE G2446 NOT-FALSIFY-TAUT T)
(TOGGLE G2447 APPEND-NLISTP T)
(TOGGLE G2448 FALSIFY-TAUT T)
(TOGGLE G2449 FORMULA-CASES T)
(TOGGLE G2450 FORMULA-CASES1 T)
(TOGGLE G2451 PROP-ATOMP-FALSIFY T)
(TOGGLE G2453 PROP-ATOMP-AUXLIST T)
(TOGGLE G2454 PROP-ATOMP-LIST T)
(TOGGLE G2455 FALSIFY-STEP T)
(TOGGLE G2456 FALSIFY T)
(TOGGLE G2457 NOT-EVAL-PROP-ATOMP T)
(TOGGLE G2458 TAUT-EVAL T)
(TOGGLE G2459 EVAL-DBLE-NEG-TYPE T)
(TOGGLE G2460 EVAL-NOR-TYPE T)
(TOGGLE G2461 EVAL-OR-TYPE T)
(TOGGLE G2463 EVAL-PROP-ATOMP T)
(TOGGLE G2464 NEG-LIST-EVAL T)
(TOGGLE G2465 EVAL-NEG-ELEM-FORM T)
(TOGGLE G2471 ELEM-FORM-EVAL T)
(TOGGLE G2472 EVAL T)
(PROVE-LEMMA EVAL-TAUTOLOGYP
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (EVAL (MAKE-DISJUNCT FLIST) (FALSIFY-TAUT FLIST NIL)))
                     (TAUTOLOGYP FLIST))
            ((DISABLE TAUTOLOGYP FORM-LIST FALSIFY-TAUT) (USE (TRUTHS-ARE-TAUTOLOGIES))))
(DEFN LIS-NOT (FLIST) (IF (NLISTP FLIST) NIL (CONS (F-NOT (CAR FLIST)) (LIS-NOT (CDR FLIST)))))
(DEFN TAUT-CONSEQ (FLIST EXP) (TAUTOLOGYP (APPEND (LIS-NOT FLIST) (CONS EXP NIL))))
(DEFN TAUTCONSEQ-PROOF
     (FLIST EXP PFLIST)
     (LIST-DETACH-PROOF FLIST EXP PFLIST (TAUT-PROOF (APPEND (LIS-NOT FLIST) (CONS EXP NIL)))))
(PROVE-LEMMA LIST-IMPLIES-REDUC
            (REWRITE)
            (EQUAL (LIST-IMPLIES FLIST EXP)
                   (MAKE-DISJUNCT (APPEND (LIS-NOT FLIST) (CONS EXP NIL)))))
(PROVE-LEMMA APPEND-EXP-FORM-LIST
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (FORMULA EXP T 0))
                     (FORM-LIST (APPEND (LIS-NOT FLIST) (CONS EXP NIL))))
            ((DISABLE FORMULA)))
(PROVE-LEMMA TAUT-CONSEQ-PROVES
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (FORMULA EXP T 0)
                          (TAUT-CONSEQ FLIST EXP)
                          (PROVES-LIST PFLIST FLIST))
                     (PROVES (TAUTCONSEQ-PROOF FLIST EXP PFLIST) EXP)))
(TOGGLE G0276 TAUTCONSEQ-PROOF T)
(PROVE-LEMMA EVAL-TAUTCONSEQ
            (REWRITE)
            (IMPLIES (AND (FORM-LIST FLIST)
                          (FORMULA EXP T 0)
                          (EVAL (MAKE-DISJUNCT (APPEND (LIS-NOT FLIST) (CONS EXP NIL)))
                                (FALSIFY-TAUT (APPEND (LIS-NOT FLIST) (CONS EXP NIL)) NIL)))
                     (TAUT-CONSEQ FLIST EXP))
            ((DISABLE TAUTOLOGYP APPEND FORMULA LIS-NOT FORM-LIST)))
(TOGGLE G0277 TAUT-CONSEQ T)
(TOGGLE G0282 FALSIFY-TAUT T)
(TOGGLE G0295 FORMULA T)
(PROVE-LEMMA EVAL-TAUTCONSEQ-PROOF-PROVES
            (REWRITE)
            (IMPLIES (AND (EVAL (MAKE-DISJUNCT (APPEND (LIS-NOT FLIST) (CONS EXP NIL)))
                                (FALSIFY-TAUT (APPEND (LIS-NOT FLIST) (CONS EXP NIL)) NIL))
                          (PROVES-LIST PFLIST FLIST)
                          (FORM-LIST FLIST)
                          (FORMULA EXP T 0))
                     (PROVES (TAUTCONSEQ-PROOF FLIST EXP PFLIST) EXP)))
(TOGGLE G0283 TAUT-CONSEQ-PROVES T)
(DEFN F-IFF-REDUC-PROOF (A B PF1 PF2) (TAUTCONSEQ-PROOF (LIST (F-IFF A B) A) B (LIST PF1 PF2)))