![[proof.png]](proof.png)
|
Main Branch (436 bytes)
((LAMBDA (T F CADR CADDR AND NOT EQUAL MEMBER THEOREM
TH1 TH2 TH THL THR TH1L TH1R TH2L TH2R TH11)
(THEOREM
(QUOTE (ARROW ((OR A (NOT B)))
((IMPLIES (AND P Q)
(EQUIV P Q)))))))
(QUOTE T)
(QUOTE NIL)
(QUOTE (LAMBDA (X) (CAR (CDR X))))
(QUOTE (LAMBDA (X) (CADR (CDR X))))
(QUOTE (LAMBDA (P Q) (COND (P (COND (Q T) (T F)) (T F)))))
(QUOTE (LAMBDA (P) (COND (P F) (T T))))
(QUOTE (LAMBDA (X Y)
(COND ((ATOM X)
(COND ((ATOM Y) (EQ X Y))
(T F)))
((EQUAL (CAR X) (CAR Y))
(EQUAL (CDR X) (CDR Y)))
(T F))))
(QUOTE (LAMBDA (X Y)
(COND ((EQ Y NIL) F)
((EQUAL X (CAR Y)) T)
(T (MEMBER X (CDR Y))))))
(QUOTE (LAMBDA (S)
(TH1 NIL NIL (CADR S) (CADDR S))))
(QUOTE (LAMBDA (A1 A2 A C)
(COND ((EQ A NIL)
(TH2 A1 A2 NIL NIL C))
((MEMBER (CAR A) C) T)
((COND
((ATOM (CAR A))
(TH1 (COND ((MEMBER (CAR A) A1) A1)
(T (CONS (CAR A) A1)))
A2 (CDR A) C))
(T (TH1 A1
(COND ((MEMBER (CAR A) A2) A2)
(T (CONS (CAR A) A2)))
(CDR A) C)))
T)
(T F))))
(QUOTE (LAMBDA (A1 A2 C1 C2 C)
(COND ((EQ C NIL) (TH A1 A2 C1 C2))
((ATOM (CAR C))
(TH2 A1 A2
(COND
((MEMBER (CAR C) C1) C1)
(T (CONS (CAR C) C1)))
C2 (CDR C)))
(T (TH2 A1 A2 C1
(COND ((MEMBER (CAR C) C2) C2)
(T (CONS (CAR C) C2)))
(CDR C))))))
(QUOTE (LAMBDA (A1 A2 C1 C2)
(COND ((EQ A2 NIL)
(AND (NOT (EQ C2 NIL))
(THR (CAR C2) A1 A2 C1 (CDR C2))))
(T (THL (CAR A2) A1 (CDR A2) C1 C2)))))
(QUOTE (LAMBDA (U A1 A2 C1 C2)
(COND ((EQ (CAR U) (QUOTE NOT))
(TH1R (CADR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE AND))
(TH2L (CDR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE OR))
(AND (TH1L (CADR U) A1 A2 C1 C2)
(TH1L (CADDR U) A1 A2 C1 C2) ))
((EQ (CAR U) (QUOTE IMPLIES))
(AND (TH1L (CADDR U) A1 A2 C1 C2)
(TH1R (CADR U) A1 A2 C1 C2) ))
((EQ (CAR U) (QUOTE EQUIV))
(AND (TH2L (CDR U) A1 A2 C1 C2)
(TH2R (CDR U) A1 A2 C1 C2))))))
(QUOTE (LAMBDA (U A1 A2 C1 C2)
(COND ((EQ (CAR U) (QUOTE NOT))
(TH1L (CADR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE AND))
(AND (TH1R (CADR U) A1 A2 C1 C2)
(TH1R (CADDR U) A1 A2 C1 C2) ))
((EQ (CAR U) (QUOTE OR))
(TH2R (CDR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE IMPLIES))
(TH11 (CADR U) (CADDR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE EQUIV))
(AND (TH11 (CADR U) (CADDR U) A1 A2 C1 C2)
(TH11 (CADDR U) (CADR U) A1 A2 C1 C2))))))
(QUOTE (LAMBDA (V A1 A2 C1 C2)
(COND ((ATOM V)
(COND ((MEMBER V C1) T)
((TH (CONS V A1) A2 C1 C2) T)
(T F)))
((MEMBER V C2) T)
((TH A1 (CONS V A2) C1 C2) T)
(T F))))
(QUOTE (LAMBDA (V A1 A2 C1 C2)
(COND ((ATOM V)
(COND ((MEMBER V A1) T)
((TH A1 A2 (CONS V C1) C2) T)
(T F)))
((MEMBER V A2) T)
((TH A1 A2 C1 (CONS V C2)) T)
(T F))))
(QUOTE (LAMBDA (V A1 A2 C1 C2)
(COND ((ATOM (CAR V))
(COND ((MEMBER (CAR V) C1) T)
((TH1L (CADR V) (CONS (CAR V) A1) A2 C1 C2) T)
(T F)))
((MEMBER (CAR V) C2) T)
((TH1L (CADR V) A1 (CONS (CAR V) A2) C1 C2) T)
(T F))))
(QUOTE (LAMBDA (V A1 A2 C1 C2)
(COND
((ATOM (CAR V))
(COND ((MEMBER (CAR V) A1) T)
((TH1R (CADR V) A1 A2 (CONS (CAR V) C1) C2) T)
(T F)))
((MEMBER (CAR V) A2) T)
((TH1R (CADR V) A1 A2 C1 (CONS (CAR V) C2)) T)
(T F))))
(QUOTE (LAMBDA (V1 V2 A1 A2 C1 C2)
(COND ((ATOM V1)
(COND ((MEMBER V1 C1) T)
((TH1R V2 (CONS V1 A1) A2 C1 C2) T)
(T F)))
((MEMBER V1 C2) T)
((TH1R V2 A1 (CONS V1 A2) C1 C2) T)
(T F)))))
|
Friendly Branch (498 bytes)
(DEFINE T . T)
(DEFINE F . NIL)
(DEFINE CADR . (LAMBDA (X) (CAR (CDR X))))
(DEFINE CADDR . (LAMBDA (X) (CADR (CDR X))))
(DEFINE AND . (LAMBDA (P Q) (COND (P (COND (Q T) (T F)) (T F)))))
(DEFINE NOT . (LAMBDA (P) (COND (P F) (T T))))
(DEFINE EQUAL .
(LAMBDA (X Y)
(COND ((ATOM X)
(COND ((ATOM Y) (EQ X Y))
(T F)))
((EQUAL (CAR X) (CAR Y))
(EQUAL (CDR X) (CDR Y)))
(T F))))
(DEFINE MEMBER .
(LAMBDA (X Y)
(COND ((EQ Y NIL) F)
((EQUAL X (CAR Y)) T)
(T (MEMBER X (CDR Y))))))
(DEFINE THEOREM .
(LAMBDA (S)
(TH1 NIL NIL (CADR S) (CADDR S))))
(DEFINE TH1 .
(LAMBDA (A1 A2 A C)
(COND ((EQ A NIL)
(TH2 A1 A2 NIL NIL C))
((MEMBER (CAR A) C) T)
((COND
((ATOM (CAR A))
(TH1 (COND ((MEMBER (CAR A) A1) A1)
(T (CONS (CAR A) A1)))
A2 (CDR A) C))
(T (TH1 A1
(COND ((MEMBER (CAR A) A2) A2)
(T (CONS (CAR A) A2)))
(CDR A) C)))
T)
(T F))))
(DEFINE TH2 .
(LAMBDA (A1 A2 C1 C2 C)
(COND ((EQ C NIL) (TH A1 A2 C1 C2))
((ATOM (CAR C))
(TH2 A1 A2
(COND
((MEMBER (CAR C) C1) C1)
(T (CONS (CAR C) C1)))
C2 (CDR C)))
(T (TH2 A1 A2 C1
(COND ((MEMBER (CAR C) C2) C2)
(T (CONS (CAR C) C2)))
(CDR C))))))
(DEFINE TH .
(LAMBDA (A1 A2 C1 C2)
(COND ((EQ A2 NIL)
(AND (NOT (EQ C2 NIL))
(THR (CAR C2) A1 A2 C1 (CDR C2))))
(T (THL (CAR A2) A1 (CDR A2) C1 C2)))))
(DEFINE THL .
(LAMBDA (U A1 A2 C1 C2)
(COND ((EQ (CAR U) (QUOTE NOT))
(TH1R (CADR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE AND))
(TH2L (CDR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE OR))
(AND (TH1L (CADR U) A1 A2 C1 C2)
(TH1L (CADDR U) A1 A2 C1 C2) ))
((EQ (CAR U) (QUOTE IMPLIES))
(AND (TH1L (CADDR U) A1 A2 C1 C2)
(TH1R (CADR U) A1 A2 C1 C2) ))
((EQ (CAR U) (QUOTE EQUIV))
(AND (TH2L (CDR U) A1 A2 C1 C2)
(TH2R (CDR U) A1 A2 C1 C2))))))
(DEFINE THR .
(LAMBDA (U A1 A2 C1 C2)
(COND ((EQ (CAR U) (QUOTE NOT))
(TH1L (CADR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE AND))
(AND (TH1R (CADR U) A1 A2 C1 C2)
(TH1R (CADDR U) A1 A2 C1 C2) ))
((EQ (CAR U) (QUOTE OR))
(TH2R (CDR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE IMPLIES))
(TH11 (CADR U) (CADDR U) A1 A2 C1 C2))
((EQ (CAR U) (QUOTE EQUIV))
(AND (TH11 (CADR U) (CADDR U) A1 A2 C1 C2)
(TH11 (CADDR U) (CADR U) A1 A2 C1 C2))))))
(DEFINE TH1L .
(LAMBDA (V A1 A2 C1 C2)
(COND ((ATOM V)
(COND ((MEMBER V C1) T)
((TH (CONS V A1) A2 C1 C2) T)
(T F)))
((MEMBER V C2) T)
((TH A1 (CONS V A2) C1 C2) T)
(T F))))
(DEFINE TH1R .
(LAMBDA (V A1 A2 C1 C2)
(COND ((ATOM V)
(COND ((MEMBER V A1) T)
((TH A1 A2 (CONS V C1) C2) T)
(T F)))
((MEMBER V A2) T)
((TH A1 A2 C1 (CONS V C2)) T)
(T F))))
(DEFINE TH2L .
(LAMBDA (V A1 A2 C1 C2)
(COND ((ATOM (CAR V))
(COND ((MEMBER (CAR V) C1) T)
((TH1L (CADR V) (CONS (CAR V) A1) A2 C1 C2) T)
(T F)))
((MEMBER (CAR V) C2) T)
((TH1L (CADR V) A1 (CONS (CAR V) A2) C1 C2) T)
(T F))))
(DEFINE TH2R .
(LAMBDA (V A1 A2 C1 C2)
(COND
((ATOM (CAR V))
(COND ((MEMBER (CAR V) A1) T)
((TH1R (CADR V) A1 A2 (CONS (CAR V) C1) C2) T)
(T F)))
((MEMBER (CAR V) A2) T)
((TH1R (CADR V) A1 A2 C1 (CONS (CAR V) C2)) T)
(T F))))
(DEFINE TH11 .
(LAMBDA (V1 V2 A1 A2 C1 C2)
(COND ((ATOM V1)
(COND ((MEMBER V1 C1) T)
((TH1R V2 (CONS V1 A1) A2 C1 C2) T)
(T F)))
((MEMBER V1 C2) T)
((TH1R V2 A1 (CONS V1 A2) C1 C2) T)
(T F))))
(THEOREM
(QUOTE (ARROW (P) ((OR P Q)))))
(THEOREM
(QUOTE (ARROW ((OR A (NOT B)))
((IMPLIES (AND P Q)
(EQUIV P Q))))))
|