;;;
;;; This file contains the data access functions for proofs and
;;; refutations as data objects, as used by the Wang theorem prover.
;;;

proof-p[proof-or-refutation] =
  [eq[second[proof-or-refutation]; "verified-by"] --> T;
   otherwise --> eq[second[proof-or-refutation]; "reduces-by"]]

make-simple-proof[conjecture; prop] =
  list4[conjecture; "verified-by"; "Rule1A"; list1[prop]]

list6[e1; e2; e3; e4; e5; e6] =
  cons[e1; cons[e2; list4[e3; e4; e5; e6]]]
  
list8[e1; e2; e3; e4; e5; e6; e7; e8] =
  cons[e1; cons[e2; list6[e3; e4; e5; e6; e7; e8]]]
    
make-linear-proof[conjecture; rule; formula; subproof] =
  list6[conjecture; "reduces-by"; rule; formula; "to"; subproof]

make-double-proof[conjecture; rule; formula; subproof1; subproof2] =
  list8[conjecture; "reduces-by"; rule; formula; "to"; subproof1; "and";
        subproof2]

make-simple-refutation[conjecture] =
  list3[conjecture; "refuted-by"; "Rule1B"]

make-linear-refutation[conjecture; rule; formula; subrefutation] =
  list6[conjecture; "refuted-by"; rule; formula; "to"; subrefutation]

make-conjecture[hypotheses; goals] =
  list4["Assuming"; hypotheses; "conclude"; goals]

hypotheses[conj] = second[conj]

goals[conj] = fourth[conj]

rule2A = "Rule2A"

rule2B = "Rule2B"

rule3A = "Rule3A"

rule3B = "Rule3B"

rule4A = "Rule4A"

rule4B = "Rule4B"

rule5A = "Rule5A"

rule5B = "Rule5B"

rule6A = "Rule6A"

rule6B = "Rule6B"