; $Id: test.scm 2345 2009-11-13 11:41:13Z schwicht $
; This file is intended as a general test.

; (load "~/minlog/init.scm")

; Contents
; 1. Preliminaries (list.scm and gen-app.scm)
; 2. Types (typ.scm)
; 3. Variables (var.scm)
; 4. Constants (pconst.scm)
; 5. Predicates (psym.scm)
; 6. Terms (term.scm and pp.scm)
; 7. Formulas and comprehension terms (formula.scm and boole.scm)
; 8. and 9. Assumption variables and axioms (axiom.scm)
; 10. Proofs (proof.scm)
; 11. Partial proofs (pproof.scm)
; 13. Automated propositional proofs (prop.scm)
; 16. Extracted terms (ets.scm and etsd.scm)
; 17. A-translation (atr.scm)


; 1. Preliminaries
; ================
; (list.scm and gen-app.scm)


; 2. Types
; ========
; (typ.scm)

; Tests of add-algs (introducing free algebras)

(add-alg "nat" '("Zero" "nat") '("Succ" "nat=>nat"))

(add-alg "ordl" '("OrdZero" "ordl") '("OrdSup" "(nat=>ordl)=>ordl"))

(add-param-alg "list" 'prefix-typeop
	       '("Nil" "list")
	       '("Cons" "alpha1=>list=>list"))

(add-param-alg "ytensor" 'tensor-typeop
	       '("TensorPair" "alpha1=>alpha2=>ytensor")) 

; (add-param-alg "ypair" 'prod-typeop
; 	       '("CartPair" "(unit=>alpha1)=>(unit=>alpha2)=>unit=>ypair"))

(add-param-alg "yplus" 'sum-typeop
	       '("Inleft" "alpha1=>yplus")
	       '("Inright" "alpha2=>yplus"))

(add-algs (list "tree" "tlist")
	  '("Leaf" "tree")
	  '("Branch" "tlist=>tree")
	  '("Empty" "tlist")
	  '("Tcons" "tree=>tlist=>tlist"))

(add-param-algs (list "labtree" "labtlist") 'alg-typeop 2
		'("LabLeaf" "alpha1=>labtree")
		'("LabBranch" "labtlist=>alpha2=>labtree")
		'("LabEmpty" "labtlist")
		'("LabTcons" "labtree=>labtlist=>labtlist"))

; An ordinal notation scheme by W. Buchholz:

(add-algs (list "hterm" "htermlist" "term")
	  '("One" "hterm")
	  '("Dn" "nat=>term=>hterm")
	  '("Hempty" "htermlist")
	  '("Hcons" "hterm=>htermlist=>htermlist")
	  '("Seq" "htermlist=>term"))

; An example for an infinitary algebra (s. ~benl/demo2.scm)

(add-algs (list "inftree" "inftlist")
	  '("Newleaf" "nat=>inftree")
          '("Infbranch" "nat=>inftlist=>inftree")
          '("Lim" "nat=>(nat=>inftree)=>inftree")
          '("Emptyinftlist" "inftlist")
          '("Inftcons" "inftree=>inftlist=>inftlist"))

; (add-alg "nix" '("Gen" "nix=>nix"))
; add-algebras-with-parameters
; nullary constructor missing for type(s)
; (arrow (alg nix) (alg nix))

(finalg? (py "nat")) ;#t
(finalg? (py "ordl")) ;#f
(finalg? (py "list nat")) ;#t
(finalg? (py "list alpha")) ;#f
(finalg? (py "nat ytensor boole")) ;#t
(finalg? (py "nat ytensor alpha")) ;#f
(finalg? (py "nat yplus boole")) ;#t
(finalg? (py "nat yplus alpha")) ;#f
(finalg? (py "tree")) ;#t
(finalg? (py "tlist")) ;#t
(finalg? (py "labtree nat boole")) ;#t
(finalg? (py "labtlist nat boole")) ;#t
(finalg? (py "labtree nat alpha")) ;#f
(finalg? (py "labtlist nat alpha")) ;#f
(finalg? (py "hterm")) ;#t
(finalg? (py "inftlist")) ;#f

(sfinalg? (py "list alpha")) ;#t
(sfinalg? (py "ordl")) ;#f
(sfinalg? (py "nat ytensor alpha")) ;#t
(sfinalg? (py "nat yplus alpha")) ;#t
(sfinalg? (py "labtree nat alpha")) ;#t
(sfinalg? (py "labtlist nat alpha")) ;#t
(sfinalg? (py "inftlist")) ;#f

(remove-alg-name "nat" "ordl" "list" "ytensor" "yplus" "tree"
		 "labtree" "hterm"
		 "inftree")

; 3. Variables
; ============
; (var.scm)


; 4. Constants
; ============
; (pconst.scm)

; tree tlist example with parameter on the leafs, as in pc07

(add-param-algs (list "tree" "tlist") 'prefix-typeop 1
		'("Leaf" "alpha1=>tree")
		'("Branch" "tlist=>tree")
		'("Empty" "tlist")
		'("Tcons" "tree=>tlist=>tlist"))

(add-alg "nat" '("Zero" "nat") '("Succ" "nat=>nat"))

; Tests for (constructor-type-to-step-type type alg-names-with-val-types)

(for-each
 (lambda (type) (pp (constructor-type-to-step-type
		     type (list (list "tree" (py "boole"))
				(list "tlist" (py "nat"))))))
 (map typed-constr-name-to-type
      (apply append (map alg-name-to-typed-constr-names
			 (alg-name-to-simalg-names "tree")))))

; alpha1=>boole
; tlist alpha1=>nat=>boole
; nat
; tree alpha1=>tlist alpha1=>boole=>nat=>nat

(for-each
 (lambda (type) (pp (constructor-type-to-step-type
		     type (list (list "tlist" (py "nat"))))))
 (map typed-constr-name-to-type
      (apply append (map alg-name-to-typed-constr-names
			 (list "tlist")))))

; nat
; tlist alpha1=>nat=>nat

(for-each
 (lambda (type) (pp (constructor-type-to-step-type
		     type (list (list "tree" (py "boole"))))))
 (map typed-constr-name-to-type
      (apply append (map alg-name-to-typed-constr-names
			 (list "tree")))))

; alpha1=>boole
; boole

; Tests for
; (arrow-types-to-uninst-paramless-recop-types-and-tsubst . arrow-types)

(let* ((recop-types-and-tsubst
	(arrow-types-to-uninst-paramless-recop-types-and-tsubst
	 (py "tree unit=>boole") (py "tlist unit=>nat")))
       (recop-types (car recop-types-and-tsubst))
       (tsubst (cadr recop-types-and-tsubst)))
  (for-each pp recop-types)
  (display-substitutions tsubst))

; tree alpha1=>
; (alpha1=>alpha52)=>
; (tlist alpha1=>alpha51=>alpha52)=>
; alpha51=>(tree alpha1=>tlist alpha1=>alpha52=>alpha51=>alpha51)=>alpha52
; tlist alpha1=>
; (alpha1=>alpha52)=>
; (tlist alpha1=>alpha51=>alpha52)=>
; alpha51=>(tree alpha1=>tlist alpha1=>alpha52=>alpha51=>alpha51)=>alpha51
; ; Type substitution:
; ; alpha1	->	unit
; ; alpha52	->	boole
; ; alpha51	->	nat
  
(let* ((recop-types-and-tsubst
	(arrow-types-to-uninst-paramless-recop-types-and-tsubst
	 (py "tlist unit=>nat")))
       (recop-types (car recop-types-and-tsubst))
       (tsubst (cadr recop-types-and-tsubst)))
  (for-each pp recop-types)
  (display-substitutions tsubst))

; tlist alpha1=>alpha53=>(tlist alpha1=>alpha53=>alpha53)=>alpha53
; ; Type substitution:
; ; alpha1	->	unit
; ; alpha53	->	nat

(let* ((recop-types-and-tsubst
	(arrow-types-to-uninst-paramless-recop-types-and-tsubst
	 (py "tree unit=>boole")))
       (recop-types (car recop-types-and-tsubst))
       (tsubst (cadr recop-types-and-tsubst)))
  (for-each pp recop-types)
  (display-substitutions tsubst))

; tree alpha1=>(alpha1=>alpha54)=>alpha54=>alpha54
; ; Type substitution:
; ; alpha1	->	unit
; ; alpha54	->	boole

(remove-alg-name "tree")
(remove-alg-name "nat")


; 5. Predicates
; =============
; (psym.scm)

; Tests of add-ids (introducing inductively defined predicates)

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)

(add-ids (list (list "Even" (make-arity (py "nat")) "algEven"))
	 '("Even 0" "InitEven")
	 '("allnc n^(Even n^ -> Even(n^ +2))" "GenEven"))

(map car (alg-name-to-typed-constr-names "algEven"))
; ("cInitEven" "cGenEven")

(add-ids (list (list "Ev" (make-arity (py "nat")) "algEv")
	       (list "Od" (make-arity (py "nat")) "algOd"))
	 '("Ev 0" "InitEv")
	 '("allnc n^(Od n^ -> Ev(n^ +1))" "GenEv")
	 '("allnc n^(Ev n^ -> Od(n^ +1))" "GenOd"))

(map car (alg-name-to-typed-constr-names "algEv"))
; ("cInitEv" "cGenEv")
(map car (alg-name-to-typed-constr-names "algOd"))
; ("cGenOd")

; For further examples of idpredconsts we distinguish nullary /
; non-nullary ones, and those with no / nullary / non-nullary
; parameter predicates.  For the last item, a special case is that
; parameter predicates of the form {x|P x} are expected

; Examples of idpredconsts, classified according to the above criteria;
; EqD non-nullary, no parameter predicates
; OrD nullary, nullary parameter predicates
; ExD nullary, unary parameter predicate
; ExL nullary, unary parameter predicate
; PiOne unary, unary parameter predicate (supersedes NotNull)
; TrCl binary, binary parameter predicate
; Acc unary, binary parameter predicate
; ExDT nullary, unary parameter predicate, expecting {x|P x}
; Cup unary, two unary parameter predicates 
; Cap unary, two unary parameter predicates 

(add-var-name "x" "y" "z" (py "alpha"))
(add-pvar-name "P" (make-arity))
(add-pvar-name "Q" (make-arity (py "alpha")))
(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))

; In ets.scm:
; (add-ids (list (list "EqD" (make-arity (py "alpha") (py "alpha"))))
; 	 '("allnc x^ EqD x^ x^" "InitEqD"))

; Should be defined as an idpredconst not requiring witnesses, i.e.,
; without "algEqD".  Then elim should be allowed for arbitrary
; formulas, since this is a uniform one clause definition.

; Here the clauses contain the type variable alpha, which can be
; substituted by itself.

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "EqD" (list (py "alpha")) '()))

(pp (make-predicate-formula idpc (pt "x^1")  (pt "x^2")))
; "x^1 eqd x^2"

; ... or else can be substituted e.g. by nat

(define idpc-inst
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "EqD" (list (py "nat")) '()))

(pp (make-predicate-formula idpc-inst (pt "n1") (pt "n2")))
; "n1 eqd n2"

; In ets.scm:
; (add-ids (list (list "OrD" (make-arity) "algOrD"))
; 	 '("P1 -> OrD" "InlOrD")
; 	 '("P2 -> OrD" "InrOrD"))

(map car (alg-name-to-typed-constr-names "algOrD"))
; ("cInlOrD" "cInrOrD")

; Here the clauses contain the parameter predicate variables P1 and
; P2, which can be substituted by themselves.

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "OrD" '()
   (list (make-cterm (pf "P1")) (make-cterm (pf "P2")))))

(pp (make-predicate-formula idpc))
; P1 ord P2

; ... or else can be substituted e.g. {|T} and {|F}

(define idpc-inst
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "OrD" '() (list  (make-cterm (pf "T")) (make-cterm (pf "F")))))

(pp (make-predicate-formula idpc-inst))
; T ord F

; We need two inductively defined existential quantifiers, one (ExD
; with D for double) for a kernel with computational content, and one
; (ExL) for a kernel without.  The reason is to avoid garbage in
; extracted programs.

; In ets.scm:
; (add-ids (list (list "ExD" (make-arity) "algExD"))
; 	 '("all x^(Q x^ -> ExD)" "InitExD"))

(define idpc (predicate-form-to-predicate (pf "exd n n=m")))
(idpredconst-to-string idpc)
; "exd n n=m"

; ExL should be formulated with uniform implication Q x^ --> instead
; of Q^'x^ ->.  It should be called ExL

; (add-ids (list (list "ExL" (make-arity) "algExL"))
; 	 '("all x^(Q^'x^ -> ExL)" "InitExL")) 

; (define idpc (predicate-form-to-predicate (pf "exl n n=m")))
; (idpredconst-to-string idpc)
; ; "exl n n=m"

(add-ids (list (list "PiOne" (make-arity (py "alpha")) "algPiOne"))
	 '("all x^,y^(R x^ y^ -> PiOne x^)" "InitPiOne"))

; PiOne stands for projection on the first component.  PiOne is
; definable from ExD, since (PiOne (cterm (x^ y^)R x^ y^))x^ is
; equivalent to (ExD (cterm (x^) R x^ y^)

; - the transitive closure of a relation.

(add-ids (list (list "TrCl" (make-arity (py "alpha") (py "alpha")) "algTrCl"))
	 '("allnc x^,y^(R x^ y^ -> TrCl x^ y^)" "InitTrCl")
	 '("allnc x^,y^,z^(R x^ y^ -> TrCl y^ z^ -> TrCl x^ z^)" "GenTrCl"))

(add-ids (list (list "Acc" (make-arity (py "alpha")) "algAcc"))
	 '("allnc x^(F -> Acc x^)" "EfqAcc")
	 '("allnc x^(all y^(R y^ x^ -> Acc y^) -> Acc x^)" "GenAccSup"))

(map car (alg-name-to-typed-constr-names "algAcc"))
; ("cEfqAcc" "cGenAccSup")

; Here the clauses contain the type variable alpha and the parameter
; predicate variable R, which can be substituted by themselves.

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "Acc"
   (list (py "alpha"))
   (list (make-cterm (pv "x^1") (pv "x^2") (pf "R x^1 x^2")))))

(pp (make-predicate-formula idpc (pt "x^3")))
; (Acc (cterm (x^1,x^2) R x^1 x^2))x^3

; ... or else can be substituted e.g. by nat and {n1,n2|n1<n2}

(define idpc-inst
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "Acc"
   (list (py "nat"))
   (list (make-cterm (pv "n1") (pv "n2") (pf "n1<n2")))))

(pp (make-predicate-formula idpc-inst (pt "n3")))
; (Acc (cterm (n1,n2) n1<n2))n3

; In ets.scm:
; (add-ids (list (list "ExDT" (make-arity) "algExDT"))
; 	 '("all x(Q x -> ExDT)" "InitExDT"))

(add-ids (list (list "Cup" (make-arity (py "alpha")) "algCup"))
	 '("all x^(Q1 x^ -> Cup x^)" "InlCup")
	 '("all x^(Q2 x^ -> Cup x^)" "InrCup"))

(add-ids (list (list "Cap" (make-arity (py "alpha")) "algCap"))
	 '("all x^(Q1 x^ -> Q2 x^ -> Cap x^)" "InitCap"))

; There are many variants: -> and/or all may be uniform, we may use a
; total variable x instead of x^, and we can have xs rather than x.

(remove-var-name "x" "y" "z")
(remove-pvar-name "P" "Q" "R")
(remove-idpc-name "Even" "Ev" "PiOne" "TrCl" "Acc" "Cup" "Cap")


; 6. Terms
; ========
; (term.scm and pp.scm)

; Tests for match2

(add-var-name "x" (py "alpha"))
(add-pvar-name "Q" (make-arity (py "alpha")))

(display-substitutions (match2 (pf "Q x^") (pf "Total x^")))
; Predicate substitution:
; Q	->	(cterm (x^) Total x^)

(display-substitutions (match2 (pf "(Pvar unit) unit^") (pf "Total x^")))
; Predicate substitution:
; (Pvar unit)	->	(cterm (unit^61) Total x^)

(display-substitutions (match2 (pf "Total x^") (pf "Total unit^")))
; Type substitution:
; alpha	->	unit
; Substitution:
; x^	->	unit^

(remove-var-name "x")
(remove-pvar-name "Q")

; Ranzi's examples:

(display-substitutions
 (match2
  (pf "(Pvar boole)boole12")
  (pf "boole12=boole12")))
; Predicate substitution:
; (Pvar boole)	->	(cterm (boole12) boole12=boole12)

(display-substitutions
 (match2
  (pf "(Pvar boole)boole^12")
  (pf "Equal boole^12 boole^12")))
; Predicate substitution:
; (Pvar boole)	->	(cterm (boole^12) Equal boole^12 boole^12)

; Tests for unfold-simplified-simrec-appterm

(add-param-algs (list "tree" "tlist") 'prefix-typeop 1
		'("Leaf" "alpha1=>tree")
		'("Branch" "tlist=>tree")
		'("Empty" "tlist")
		'("Tcons" "tree=>tlist=>tlist"))

(add-var-name "u" "v" (py "tree alpha1"))
(add-var-name "us" "vs" (py "tlist alpha1"))
(add-var-name "a" "b" (py "tree unit"))
(add-var-name "as" "bs" (py "tlist unit"))

(pp (unfold-simplified-simrec-appterm
     (pt "(Rec tlist unit=>nat)as 0([bs,n]Succ n)")))
; (Rec tlist unit=>nat tree unit=>tree unit)as([unit2312](Leaf unit)unit2312)
; ([as2310,n2311](Branch unit)as2310)
; 0
; ([a2308,bs,a2309,n]Succ n)

(pp (nt (unfold-simplified-simrec-appterm
	 (pt "(Rec tlist unit=>nat)as 0([bs,n]Succ n)"))))
; (Rec tlist unit=>nat)as 0([as1]Succ)

; Test for simplify-simrec-appterm

(pp (simplify-simrec-appterm
     (pt "(Rec tlist unit=>nat tree unit=>tree unit)as
          (Leaf unit)
          ([as0,n1](Branch unit)as0)
          0
          ([a0,as1,a2,n]Succ n)")))
; (Rec tlist unit=>nat)as 0([as1,n]Succ n)

(remove-var-name "u" "v")
(remove-var-name "us" "vs")
(remove-var-name "a" "b")
(remove-var-name "as" "bs")

(remove-alg-name "tree")


; 7. Formulas and comprehension terms
; ===================================
; (formula.scm and boole.scm)


(add-var-name "x" "y" (py "alpha"))
(add-pvar-name "Q" (make-arity (py "alpha")))

; In ets.scm:
; (add-ids (list (list "ExD" (make-arity) "algExD"))
; 	 '("all x^(Q x^ -> ExD)" "InitExD"))

(define formula (pf "exd boole1(boole1=boole2 -> Q alpha)"))
(define formula (pf "exd x1(Equal x1 x2 -> Q x3)"))

(map var-to-string (formula-to-free formula))
(map tvar-to-string (formula-to-tvars formula))
(map pvar-to-string (formula-to-pvars formula))

; Tests for formula-substitute

(add-var-name "x" "y" (py "alpha"))
(add-pvar-name "Q" (make-arity (py "alpha")))

(pp (formula-subst formula (py "alpha") (py "unit")))

(pp (formula-substitute
     (pf "Total x^")
     (list (list (py "alpha") (py "boole")))))

(pp (formula-substitute
     (pf "Q x")
     (list (list (pv "x") (pt "y")))))

(pp (formula-substitute
     (pf "Q x")
     (list (list (predicate-form-to-predicate (pf "Q x"))
		 (make-cterm (pv "x") (pf "Total x"))))))
; Total x

(pp (formula-substitute
     (pf "Q x^")
     (list (list (predicate-form-to-predicate (pf "Q x^"))
		 (make-cterm (pv "x^") (pf "Equal x^ x^"))))))
; Equal x^ x^

(pp (formula-substitute
     (pf "Q x^")
     (list (list (predicate-form-to-predicate (pf "Q x^"))
		 (make-cterm (pv "x") (pf "Equal x x"))))))
; Total x^ & Equal x^ x^
; because this is how we understand {x|Equal x x} as opposed to
; {x^ | Equal x^ x^}.

; Testing substitution in prime formulas built from idpredconsts (that
; is, in the parameter cterms in those, and in the arguments)

(pp (formula-substitute
;      (pf "(ExD alpha (cterm (x^) Equal x^ x^))")
     (pf "exd x^ Equal x^ x^")
     (list (list (py "alpha") (py "boole")))))
; exd boole^112 Equal boole^112 boole^112
    
(pp (formula-substitute
     (pf "exd x^ Q x^")
     (list (list (predicate-form-to-predicate (pf "Q x^"))
		 (make-cterm (pv "x^") (pf "Equal x^ x^"))))))
; exd x^ Equal x^ x^
    
(pp (formula-substitute
;      (pf "(ExD alpha (cterm (x^) Q x^))")
     (pf "exd x^ Q x^")
     (list (list (predicate-form-to-predicate (pf "Q x^"))
		 (make-cterm (pv "x") (pf "Equal x x"))))))
; exd x Equal x x
; But notice that ExD has its clause with x^ .  It is only ExDT
; which has its clause with x

; In ets.scm
; (add-ids (list (list "ExDT" (make-arity) "algExDT"))
; 	 '("all x(Q x -> ExDT)" "InitExDT"))

(pp (formula-substitute
     (pf "(ExDT alpha (cterm (x) Q x))")
     (list (list (predicate-form-to-predicate (pf "Q x^"))
		 (make-cterm (pv "x") (pf "Equal x x"))))))

(remove-var-name "x" "y")
(remove-pvar-name "Q")

(define testformula1
  (pf "all n allnc m(exca n1 n=n1 -> excl m1,m2(m1=m2 and F))"))

(formula-to-free testformula1)
(ex-free-formula? testformula1)
(pp (nbe-formula-to-type testformula1))
(length (formula-to-prime-subformulas testformula1))

(alpha-equal-formulas-to-renaming
 (pf "all boole allnc unit(exca boole1 boole=boole1 ->
                           excl unit1,unit2(unit1=unit2 and F))")
 (pf "all boole allnc unit(exca boole1 boole=boole1 ->
                           excl unit1,unit3(unit1=unit3 and F))"))

(var-to-string
 (var-and-vars-to-new-var
  (pv "n100") (list (pv "n") (pv "n2") (pv "n19")(pv "n1") (pv "m0"))))
; "n0"

(pp (aconst-to-formula (all-formulas-to-ind-aconst (pf "all n n=n"))))

; all n2067(
;  0=0 -> all n2068(n2068=n2068 -> Succ n2068=Succ n2068) -> n2067=n2067)

(pp (rename-variables
     (aconst-to-formula (all-formulas-to-ind-aconst (pf "all n n=n")))))

; all n(0=0 -> all n0(n0=n0 -> Succ n0=Succ n0) -> n=n)

(pp (aconst-to-formula (all-formula-to-gind-aconst (pf "all n n=n") 1)))

; all (nat=>nat)_2071,n2072(
;  all n2072(
;   all n2073((nat=>nat)_2071 n2073<(nat=>nat)_2071 n2072 -> n2073=n2073) -> 
;   n2072=n2072) -> 
;  all boole(boole -> n2072=n2072))

(pp (rename-variables
     (aconst-to-formula (all-formula-to-gind-aconst (pf "all n n=n") 1))))

; all (nat=>nat),n(
;  all n0(all n0((nat=>nat)n0<(nat=>nat)n0 -> n0=n0) -> n0=n0) -> 
;  all boole0(boole0 -> n=n))


; 8. and 9. Assumption variables and axioms
; =========================================
; (axiom.scm)

(add-param-alg "list" 'prefix-typeop
	       '("Nil" "list")
	       '("Cons" "alpha1=>list=>list"))

(add-pvar-name "P" (make-arity (py "nat")))

(pp (caar (all-formulas-to-uninst-imp-formulas-and-tpinst
	   (pf "all n^(STotal n^ -> P n^)"))))
; all n^1284(
;  STotal n^1284 -> 
;  P298 0 -> all n1285(P298 n1285 -> P298(Succ n1285)) -> P298 n^1284)

(remove-pvar-name "P")

(add-pvar-name "P" (make-arity (py "list nat")))
(add-var-name "ns" (py "list nat"))

(pp (caar (all-formulas-to-uninst-imp-formulas-and-tpinst
	   (pf "all ns^(STotal ns^ -> P ns^)"))))
; all (list alpha15)^1330(
;  (STotal alpha15)(list alpha15)^1330 -> 
;  (Pvar list alpha15)_311(Nil alpha15) -> 
;  all alpha15^1332,(list alpha15)^1331(
;   (STotal alpha15)(list alpha15)^1331 -> 
;   (Pvar list alpha15)_311(list alpha15)^1331 -> 
;   (Pvar list alpha15)_311((Cons alpha15)alpha15^1332(list alpha15)^1331)) -> 
;  (Pvar list alpha15)_311(list alpha15)^1330)

(display-substitutions
 (cadr (all-formulas-to-uninst-imp-formulas-and-tpinst
	(pf "all ns^(STotal ns^ -> P ns^)"))))
; Type substitution:
; alpha13	->	nat
; Predicate substitution:
; (Pvar list alpha13)_309	->	(cterm (ns^) P ns^)

(remove-pvar-name "P")
(remove-var-name "ns")
(remove-alg-name "list")

(add-pvar-name "P" (make-arity (py "nat")))

(pp (aconst-to-formula
     (all-formulas-to-ind-aconst (pf "all n P n"))))

; all n1427(P 0 -> all n1428(P n1428 -> P(Succ n1428)) -> P n1427)

(remove-pvar-name "P")

; Simultaneously defined algebras require simultaneous induction:

(add-algs (list "tree" "tlist")
	  '("Leaf" "tree")
	  '("Branch" "tlist=>tree")
	  '("Empty" "tlist")
	  '("Tcons" "tree=>tlist=>tlist"))

(add-pvar-name "P" (make-arity (py "tree")))
(add-pvar-name "Q" (make-arity (py "tlist")))

(pp (aconst-to-formula
     (all-formulas-to-ind-aconst
      (pf "all tree P tree")
      (pf "all tlist Q tlist"))))

; all tree1450(
;  P Leaf -> 
;  all tlist1453(Q tlist1453 -> P(Branch tlist1453)) -> 
;  Q Empty -> 
;  all tree1452,tlist1451(
;   P tree1452 -> Q tlist1451 -> Q(Tcons tree1452 tlist1451)) -> 
;  P tree1450)

(remove-pvar-name "P" "Q")
(remove-alg-name "tree")

; Cases:

(add-pvar-name "P" (make-arity (py "nat")))

(pp (aconst-to-formula
     (all-formula-to-cases-aconst (pf "all n P n"))))

; all n1461(P 0 -> all n1462 P(Succ n1462) -> P n1461)

(remove-pvar-name "P")

; GInd: all h,x(all x(all y(hy<hx -> Ry) -> Rx) -> all p(p -> Rx))
; with h a measure function of type alpha1 => ... => alphan => nat.

(add-var-name "h" (py "alpha=>alpha=>nat"))
(add-var-name "x" (py "alpha"))
(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))

(pp (aconst-to-formula
     (all-formula-to-gind-aconst (pf "all x1,x2 R x1 x2") 2)))

; all h1436,x1437,x1438(
;  all x1437,x1438(
;   all x1439,x1440(h1436 x1439 x1440<h1436 x1437 x1438 -> R x1439 x1440) -> 
;   R x1437 x1438) -> 
;  all boole(boole -> R x1437 x1438))

(remove-var-name "h" "x")
(remove-pvar-name "R")

; intro and elim

(add-ids (list (list "Even" (make-arity (py "nat")) "algEven"))
	 '("Even 0" "InitEven")
	 '("allnc n^(Even n^ -> Even(n^ +2))"))

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst "Even" '() '()))

; There are no types, since the clauses do not contain type variables,
; and no cterms, since the clauses do not contain parameter predicate
; variables.

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; "Even 0"

(define aconst1 (number-and-idpredconst-to-intro-aconst 1 idpc))
(pp (aconst-to-formula aconst1))
; allnc n^(Even n^ -> Even(n^ +2))

(define eterm1 (proof-to-extracted-term (make-proof-in-aconst-form aconst1)))
(pp (term-to-type eterm1)) 
; "algEven=>algEven"

(add-pvar-name "Q" (make-arity (py "nat")))

(define aconst (imp-formulas-to-elim-aconst (pf "Even m^ -> Q m^")))
(pp (aconst-to-formula aconst))
; allnc n^1323(
;  Even n^1323 -> Q 0 -> allnc n^(Even n^ -> Q n^ -> Q(n^ +2)) -> Q n^1323)

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst)))
(pp (term-to-type eterm))
; algEven=>alpha6=>(algEven=>alpha6=>alpha6)=>alpha6

(remove-pvar-name "Q")
(remove-idpc-name "Even")

(add-ids (list (list "Ev" (make-arity (py "nat")) "algEv")
	       (list "Od" (make-arity (py "nat")) "algOd"))
	 '("Ev 0" "InitEv")
	 '("allnc n^(Od n^ -> Ev(n^ +1))" "GenEv")
	 '("allnc n^(Ev n^ -> Od(n^ +1))" "GenOd"))

(define idpcev
  (idpredconst-name-and-types-and-cterms-to-idpredconst "Ev" '() '()))
(define idpcod
  (idpredconst-name-and-types-and-cterms-to-idpredconst "Od" '() '()))

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpcev))
(pp (aconst-to-formula aconst0))
; "Ev 0"
(define aconst1 (number-and-idpredconst-to-intro-aconst 1 idpcev))
(pp (aconst-to-formula aconst1))
; allnc n^(Od n^ -> Ev(n^ +1))

(define aconst2 (number-and-idpredconst-to-intro-aconst 0 idpcod))
(pp (aconst-to-formula aconst2))
; allnc n^(Ev n^ -> Od(n^ +1))

(define eterm2 (proof-to-extracted-term (make-proof-in-aconst-form aconst2)))
(pp (term-to-type eterm2))
; algEv=>algOd

(add-pvar-name "Q" (make-arity (py "nat")))

(define aconst (imp-formulas-to-elim-aconst (pf "Ev m^ -> Q1 m^")
					    (pf "Od m^ -> Q2 m^")))
(pp (aconst-to-formula aconst))
; allnc n^1363(
;  Ev n^1363 -> 
;  Q1 0 -> 
;  allnc n^(Od n^ -> Q2 n^ -> Q1(n^ +1)) -> 
;  allnc n^(Ev n^ -> Q1 n^ -> Q2(n^ +1)) -> Q1 n^1363)

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst)))
(pp (term-to-type eterm))
; algEv=>
; alpha12=>(algOd=>alpha13=>alpha12)=>(algEv=>alpha12=>alpha13)=>alpha12

(remove-pvar-name "Q")
(remove-idpc-name "Ev")

(add-var-name "x" "y" "z" (py "alpha"))
(add-pvar-name "P" (make-arity))
(add-pvar-name "Q" (make-arity (py "alpha")))
(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))

; In ets.scm:
; (add-ids (list (list "EqD" (make-arity (py "alpha") (py "alpha")) "algEqD"))
; 	 '("allnc x^ EqD x^ x^" "InitEqD"))

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "EqD" (list (py "alpha")) '()))

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; allnc x^ x^ eqd x^

(define aconst
  (imp-formulas-to-elim-aconst
   (pf "x^1 eqd x^2 -> R x^1 x^2")))
(pp (aconst-to-formula aconst))
; allnc x^1442,x^1441(
;  x^1442 eqd x^1441 -> allnc x^ R x^ x^ -> R x^1442 x^1441)

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst)))
(pp (term-to-type eterm))
; algEqD=>alpha20=>alpha20

; In ets.scm
; (add-ids (list (list "OrD" (make-arity) "algOrD"))
; 	 '("P1 -> OrD" "InlOrD")
; 	 '("P2 -> OrD" "InrOrD"))

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "OrD" '()
   (list (make-cterm (pf "P1")) (make-cterm (pf "P2")))))

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; P1 -> P1 ord P2

(define aconst1 (number-and-idpredconst-to-intro-aconst 1 idpc))
(pp (aconst-to-formula aconst1))
; P2 -> P1 ord P2

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm))
; alpha24=>algOrD alpha24 alpha22

(define aconst
  (imp-formulas-to-elim-aconst
   (pf "P1 ord P2 -> P")))
(pp (aconst-to-formula aconst))
; P1 ord P2 -> (P1 -> P) -> (P2 -> P) -> P

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst)))
(pp (term-to-type eterm))
; algOrD alpha23 alpha21=>(alpha23=>alpha18)=>(alpha21=>alpha18)=>alpha18

; In ets.scm
; (add-ids (list (list "ExD" (make-arity) "algExD"))
; 	 '("all x^(Q x^ -> ExD)" "InitExD"))

(define idpc (predicate-form-to-predicate (pf "exd n n=m")))
(idpredconst-to-string idpc)
; "exd n n=m"

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; allnc m all n^1501(Total n^1501 & n^1501=m -> exd n n=m)

(define eterm0 (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm0))
; nat=>algExD nat unit

(define aconst (imp-formulas-to-elim-aconst (pf "exd n n=m -> k=0")))
(pp (aconst-to-formula aconst))
; allnc m,k(exd n n=m -> all n^1503(Total n^1503 & n^1503=m -> k=0) -> k=0)

(define idpc (predicate-form-to-predicate (pf "exd n^ n^ =m")))
(idpredconst-to-string idpc)
; "exd n^ n^ =m"

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; allnc m all n^1505(n^1505=m -> exd n^ n^ =m)

(define aconst (imp-formulas-to-elim-aconst (pf "exd n^ n^ =m -> k=0")))
(pp (aconst-to-formula aconst))
; allnc m,k(exd n^ n^ =m -> all n^1507(n^1507=m -> k=0) -> k=0)


; (add-ids (list (list "ExL" (make-arity) "algExL"))
; 	 '("all x^(Q^'x^ -> ExL)" "InitExL")) 

; (define idpc (predicate-form-to-predicate (pf "exl n n=m")))
; (idpredconst-to-string idpc)
; ; "exl n n=m"

; (define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
; (pp (aconst-to-formula aconst0))
; ; allnc m all n^1516(Total n^1516 & n^1516=m -> exl n n=m)

; (define eterm0 (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
; (pp (term-to-type eterm0))
; ; nat=>algExL nat

; (define aconst (imp-formulas-to-elim-aconst (pf "exl n n=m -> k=0")))
; (pp (aconst-to-formula aconst))
; ; allnc m,k(exl n n=m -> all n^1521(Total n^1521 & n^1521=m -> k=0) -> k=0)

; (define idpc (predicate-form-to-predicate (pf "exl n^ n^ =m")))
; (idpredconst-to-string idpc)
; ; "exl n^ n^ =m"

; (define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
; (pp (aconst-to-formula aconst0))
; ; allnc m all n^1523(n^1523=m -> exl n^ n^ =m)

; (define eterm0 (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
; (pp (term-to-type eterm0))
; ; nat=>algExL nat

; (define aconst (imp-formulas-to-elim-aconst (pf "exl n^ n^ =m -> k=0")))
; (pp (aconst-to-formula aconst))
; ; allnc m,k(exl n^ n^ =m -> all n^1530(n^1530=m -> k=0) -> k=0)


(add-ids (list (list "PiOne" (make-arity (py "alpha")) "algPiOne"))
	 '("all x^,y^(R x^ y^ -> PiOne x^)" "InitPiOne"))

(define idpc
  (predicate-form-to-predicate
   (pf "(PiOne (cterm (x^1535,x^1534) R x^1535 x^1534))x^")))
(idpredconst-to-string idpc)
; "(PiOne (cterm (x^1535,x^1534) R x^1535 x^1534))"

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; all x^,y^(R x^ y^ -> (PiOne (cterm (x^1544,x^1543) R x^1544 x^1543))x^)

(define eterm0 (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm0))
; alpha=>alpha=>alpha17=>algPiOne alpha alpha17

(define aconst
  (imp-formulas-to-elim-aconst
   (pf "(PiOne (cterm (x^1544,x^1543) R x^1544 x^1543))x^ -> k=0")))
(pp (aconst-to-formula aconst))
; allnc x^1552,k(
;  (PiOne (cterm (x^1554,x^1553) R x^1554 x^1553))x^1552 -> 
;  all x^,y^(R x^ y^ -> k=0) -> k=0)


(add-ids (list (list "TrCl" (make-arity (py "alpha") (py "alpha")) "algTrCl"))
	 '("allnc x^,y^(R x^ y^ -> TrCl x^ y^)" "InitTrCl")
	 '("allnc x^,y^,z^(R x^ y^ -> TrCl y^ z^ -> TrCl x^ z^)" "GenTrCl"))

(define idpc
  (predicate-form-to-predicate
   (pf "(TrCl (cterm (x^1535,x^1534) R x^1535 x^1534))x^ y^")))
(idpredconst-to-string idpc)
; "(TrCl (cterm (x^1535,x^1534) R x^1535 x^1534))"

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; allnc x^,y^(R x^ y^ -> (TrCl (cterm (x^1571,x^1570) R x^1571 x^1570))x^ y^)

(define eterm0 (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm0))
; alpha17=>algTrCl alpha17

(define aconst
  (imp-formulas-to-elim-aconst
   (pf "(TrCl (cterm (x^1535,x^1534) R x^1535 x^1534))x^ y^ -> k=0")))
(pp (aconst-to-formula aconst))
; allnc x^1580,x^1579,k(
;  (TrCl (cterm (x^1582,x^1581) R x^1582 x^1581))x^1580 x^1579 -> 
;  allnc x^,y^(R x^ y^ -> k=0) -> 
;  allnc x^,y^,z^(
;   R x^ y^ -> 
;   (TrCl (cterm (x^1582,x^1581) R x^1582 x^1581))y^ z^ -> k=0 -> k=0) -> 
;  k=0)


(add-ids (list (list "Acc" (make-arity (py "alpha")) "algAcc"))
	 '("allnc x^(F -> Acc x^)" "EfqAcc")
	 '("allnc x^(all y^(R y^ x^ -> Acc y^) -> Acc x^)" "GenAccSup"))

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "Acc"
   (list (py "alpha"))
   (list (make-cterm (pv "x^1") (pv "x^2") (pf "R x^1 x^2")))))

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; allnc x^(F -> (Acc (cterm (x^1599,x^1598) R x^1599 x^1598))x^)

(define eterm0 (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm0))
; algAcc alpha alpha17

(define aconst1 (number-and-idpredconst-to-intro-aconst 1 idpc))
(pp (aconst-to-formula aconst1))
; allnc x^(
;  all y^(R y^ x^ -> (Acc (cterm (x^1605,x^1604) R x^1605 x^1604))y^) -> 
;  (Acc (cterm (x^1605,x^1604) R x^1605 x^1604))x^)

(define eterm1 (proof-to-extracted-term (make-proof-in-aconst-form aconst1)))
(pp (term-to-type eterm1))
; (alpha=>alpha17=>algAcc alpha alpha17)=>algAcc alpha alpha17

(define aconst
  (imp-formulas-to-elim-aconst
   (pf "(Acc (cterm (x^1535,x^1534) R x^1535 x^1534))x^ -> k=0")))
(pp (aconst-to-formula aconst))
; allnc x^1611,k(
;  (Acc (cterm (x^1613,x^1612) R x^1613 x^1612))x^1611 -> 
;  allnc x^(F -> k=0) -> 
;  allnc x^(
;   all y^(R y^ x^ -> (Acc (cterm (x^1613,x^1612) R x^1613 x^1612))y^) -> 
;   all y^(R y^ x^ -> k=0) -> k=0) -> 
;  k=0)

; In ets.scm:
; (add-ids (list (list "ExDT" (make-arity) "algExDT"))
; 	 '("all x(Q x -> ExDT)" "InitExDT"))

(define idpc
  (predicate-form-to-predicate
   (pf "(ExDT nat (cterm (n) n=m))"))) 
(idpredconst-to-string idpc)
; "(ExDT nat (cterm (n) n=m))"

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; allnc m all n1619(n1619=m -> (ExDT nat (cterm (n) n=m)))

(define eterm0 (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm0))
; nat=>algExDT nat unit

(define aconst
  (imp-formulas-to-elim-aconst (pf "(ExDT nat (cterm (n) n=m)) -> k=0")))
(pp (aconst-to-formula aconst))
; allnc m,k((ExDT nat (cterm (n) n=m)) -> all n1624(n1624=m -> k=0) -> k=0)


(add-ids (list (list "Cup" (make-arity (py "alpha")) "algCup"))
	 '("all x^(Q1 x^ -> Cup x^)" "InlCup")
	 '("all x^(Q2 x^ -> Cup x^)" "InrCup"))

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "Cup" (list (py "alpha"))
   (list (make-cterm (pv "x^") (pf "Q1 x^"))
	 (make-cterm (pv "x^") (pf "Q2 x^")))))

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; all x^(
;  Q1 x^ -> (Cup (cterm (x^1637) Q1 x^1637) (cterm (x^1636) Q2 x^1636))x^)

(define aconst1 (number-and-idpredconst-to-intro-aconst 1 idpc))
(pp (aconst-to-formula aconst1))
; all x^(
;  Q2 x^ -> (Cup (cterm (x^1640) Q1 x^1640) (cterm (x^1639) Q2 x^1639))x^)

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm))
; alpha=>alpha30=>algCup alpha alpha30 alpha28

(define aconst
  (imp-formulas-to-elim-aconst
   (pf "(Cup (cterm (x^) Q1 x^) (cterm (x^) Q2 x^))x^ -> P")))
(pp (aconst-to-formula aconst))
; allnc x^1652(
;  (Cup (cterm (x^1654) Q1 x^1654) (cterm (x^1653) Q2 x^1653))x^1652 -> 
;  all x^(Q1 x^ -> P) -> all x^(Q2 x^ -> P) -> P)

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst)))
(pp (term-to-type eterm))
; algCup alpha alpha30 alpha28=>
; (alpha=>alpha30=>alpha34)=>(alpha=>alpha28=>alpha34)=>alpha34


(add-ids (list (list "Cap" (make-arity (py "alpha")) "algCap"))
	 '("all x^(Q1 x^ -> Q2 x^ -> Cap x^)" "InitCap"))

(define idpc
  (idpredconst-name-and-types-and-cterms-to-idpredconst
   "Cap" (list (py "alpha"))
   (list (make-cterm (pv "x^") (pf "Q1 x^"))
	 (make-cterm (pv "x^") (pf "Q2 x^")))))

(define aconst0 (number-and-idpredconst-to-intro-aconst 0 idpc))
(pp (aconst-to-formula aconst0))
; all x^(
;  Q1 x^ -> 
;  Q2 x^ -> (Cap (cterm (x^1669) Q1 x^1669) (cterm (x^1668) Q2 x^1668))x^)

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst0)))
(pp (term-to-type eterm))
; alpha=>alpha30=>alpha28=>algCap alpha alpha30 alpha28

(define aconst
  (imp-formulas-to-elim-aconst
   (pf "(Cap (cterm (x^) Q1 x^) (cterm (x^) Q2 x^))x^ -> P")))
(pp (aconst-to-formula aconst))
; allnc x^1677(
;  (Cap (cterm (x^1679) Q1 x^1679) (cterm (x^1678) Q2 x^1678))x^1677 -> 
;  all x^(Q1 x^ -> Q2 x^ -> P) -> P)

(define eterm (proof-to-extracted-term (make-proof-in-aconst-form aconst)))
(pp (term-to-type eterm))
; algCap alpha alpha30 alpha28=>(alpha=>alpha30=>alpha28=>alpha34)=>alpha34


(remove-var-name "x" "y" "z")
(remove-pvar-name "P" "Q" "R")
(remove-idpc-name "PiOne" "TrCl" "Acc" "Cup" "Cap")


; 10. Proofs
; ==========
; (proof.scm)

(for-each pp (cdr (proof-to-final-allnc-elim-op-and-args
		   (mk-proof-in-elim-form
		    (make-proof-in-avar-form
		     (make-avar (pf "allnc boole1,boole2,boole3 T") 7 "u"))
		    (pt "boole4")
		    (pt "boole5")
		    (pt "boole6")))))
; boole4
; boole5
; boole6

(cdp (make-proof-in-aconst-form total-aconst))

(cdp (proof-substitute
      (make-proof-in-aconst-form total-aconst)
      (list (list (py "alpha1") (py "boole"))
	    (list (py "alpha2") (py "boole=>boole")))))

; A rather general example for proof-substitute

(set! COMMENT-FLAG #f)
; (libload "nat.scm")
(libload "list.scm")
(set! COMMENT-FLAG #t)

(add-var-name "x" (py "alpha"))
(add-var-name "xs" (py "list alpha"))

(add-computation-rule (pt "Lh(Nil alpha)") (pt "Zero"))
(add-computation-rule (pt "Lh(x::xs)") (pt "Succ Lh xs"))

(add-pvar-name "Q" (make-arity (py "list alpha")))
(add-var-name "xs" (py "list alpha"))
(add-var-name "u" (py "alpha"))
(add-tvar-name "beta")
(add-pvar-name "R" (make-arity (py "nat")))

(define aconst (all-formula-to-cases-aconst (pf "all xs Q xs")))
(display-substitutions (aconst-to-tpinst aconst))

; Type substitution:
; alpha44	->	alpha
; Predicate substitution:
; (Pvar list alpha44)_462	->	(cterm (xs) Q xs)
 
; For testing, direct construction of the Cases aconst:

(define aconst0
  (make-aconst
   "Cases"
   'axiom
   (pf "all xs(Q(Nil alpha) -> all u,xs Q(u::xs) -> Q xs)")
   (list (list (py "alpha") (py "list beta"))
	 (list (make-pvar (make-arity (py "list alpha"))
			  -1 h-deg-zero n-deg-zero "Q")
	       (make-cterm (pv "list list beta")
			   (pf "Lh(list list beta)=n -> R m"))))
   (pf "all (list list beta)(Lh(list list beta)=n -> R m)")))

(display-substitutions (aconst-to-tpinst aconst0))

; Type substitution:
; alpha	->	list beta
; Predicate substitution:
; Q	->	(cterm ((list list beta)) Lh(list list beta)=n -> R m)

(cdp (proof-substitute
      (mk-proof-in-elim-form (make-proof-in-aconst-form aconst0)
			     (pt "n1") (pt "m1"))
      (list (list (py "beta") (py "boole")))))


(cdp (proof-substitute
      (mk-proof-in-elim-form (make-proof-in-aconst-form aconst0)
			     (pt "n1") (pt "m1"))
      (list (list (pv "n1") (pt "n2"))
	    (list (pv "m1") (pt "m2")))))

(cdp (proof-substitute
      (mk-proof-in-elim-form (make-proof-in-aconst-form aconst0)
			     (pt "n1") (pt "m1"))
      (list (list (py "beta") (py "boole"))
	    (list (pv "n1") (pt "n2"))
	    (list (pv "m1") (pt "m2")))))

(cdp (proof-substitute
      (mk-proof-in-elim-form (make-proof-in-aconst-form aconst0)
			     (pt "n1") (pt "m1"))
      (list (list (py "beta") (py "boole"))
	    (list (pv "n1") (pt "n2"))
	    (list (pv "m1") (pt "m2"))
	    (list (predicate-form-to-predicate (pf "R nat"))
		  (make-cterm (pv "n") (pf "n=m3"))))))

(remove-var-name "x" "xs" "u")
(remove-pvar-name "Q" "R")
(remove-tvar-name "beta")


; 11. Partial proofs
; ==================
; (pproof.scm)

; Tests for use

(add-var-name "x" (py "alpha"))
(pp "Eq-Refl")
; allnc alpha^ Equal alpha^ alpha^

(set-goal (pf "all boole Equal boole boole"))
(assume "boole")
(use "Eq-Refl")

(add-pvar-name "P" (make-arity (py "alpha")))
(add-global-assumption "MPUnary" (pf "all x(P1 x -> (P1 x -> P2 x) -> P2 x)"))

(set-goal (pf "all x1 P3 x1"))
(assume "x1")
(use "MPUnary" (make-cterm (pv "x4") (pf "Total x4")) (pt "x5"))

(remove-global-assumption "MPUnary")
(remove-pvar-name "P")

; The next example shows that error messages in use-intern in case of
; missing terms refer to the original variable in the used formula
; even if such variables had to be renamed.

(pp "Eq-Trans")

; allnc alpha^1,alpha^2,alpha^3(
;  Equal alpha^1 alpha^2 -> Equal alpha^2 alpha^3 -> Equal alpha^1 alpha^3)

(set-goal (pf "all x Equal x x"))
(assume "x")
; (use "Eq-Trans")

; use
; more terms expected, to be substituted for
; alpha^2

(use "Eq-Trans" (pt "x1"))

(remove-var-name "x")


; Tests for ind

(add-pvar-name "P" (make-arity (py "nat")))

(set-goal (pf "all n P n"))
(ind)
; ok, ?_1 can be obtained from
; ?_3: all n1423(P n1423 -> P(Succ n1423)) from
;   n1421

; ?_2: P 0 from
;   n1421

(set-goal (pf "all n^(STotal n^ -> P n^)"))
(ind)
; ok, ?_1 can be obtained from
; ?_3: all n1298(P n1298 -> P(Succ n1298)) from
;   n^1296  1:STotal n^1296

; ?_2: P 0 from
;   n^1296  1:STotal n^1296

(set-goal (pf "all n^ P n^"))
(assume "n^")
(ind (pt "n^"))
; ok, ?_2 can be obtained from
; ?_5: all n1292(P n1292 -> P(Succ n1292)) from
;   n^

; ?_4: P 0 from
;   n^

; ?_3: STotal n^ from
;   n^

(remove-pvar-name "P")

(add-alg "ordl" '("OrdZero" "ordl") '("OrdSup" "(nat=>ordl)=>ordl"))
(add-pvar-name "P" (make-arity (py "ordl")))

(set-goal (pf "all ordl P ordl"))
(ind)
; ok, ?_1 can be obtained from
; ?_3: all (nat=>ordl)_1426(
;       all n1427 P((nat=>ordl)_1426 n1427) -> P(OrdSup(nat=>ordl)_1426)) from
;   ordl1424

; ?_2: P OrdZero from
;   ordl1424

; (set-goal (pf "all ordl^(STotal ordl^ -> P ordl^)"))
; (ind)
; sfinalg-to-se-const
; structure finitary algebra expected
; ordl

(remove-pvar-name "P")
(remove-alg-name "ordl")

(add-pvar-name "P" (make-arity (py "list nat")))
(add-var-name "ns" (py "list nat"))

(set-goal (pf "all ns P ns"))
(ind)
; ok, ?_1 can be obtained from
; ?_3: all n1296,ns1297(P ns1297 -> P((Cons nat)n1296 ns1297)) from
;   ns1291

; ?_2: P(Nil nat) from
;   ns1291

(set-goal (pf "all ns^(STotal ns^ -> P ns^)"))
(ind)
; ok, ?_1 can be obtained from
; ?_3: all n^1308,ns^1309(
;       STotal ns^1309 -> P ns^1309 -> P((Cons nat)n^1308 ns^1309)) from
;   ns^1303  1:STotal ns^1303

; ?_2: P(Nil nat) from
;   ns^1303  1:STotal ns^1303

(set-goal (pf "all ns^ P ns^"))
(assume "ns^")
(ind (pt "ns^"))
; ok, ?_2 can be obtained from
; ?_5: all n^1354,ns^1355(
;        STotal ns^1355 -> P ns^1355 -> P((Cons nat)n^1354 ns^1355)) from
;   ns^

; ?_4: P(Nil nat) from
;   ns^

; ?_3: STotal ns^ from
;   ns^

(remove-pvar-name "P")
(remove-var-name "ns")

(add-pvar-name "P" (make-arity (py "list alpha")))
(add-var-name "x" (py "alpha"))
(add-var-name "xs" (py "list alpha"))

(set-goal (pf "all xs P xs"))
(ind)
; ok, ?_1 can be obtained from
; ?_3: all x1433,xs1434(P xs1434 -> P((Cons alpha)x1433 xs1434)) from
;   xs1428

; ?_2: P(Nil alpha) from
;   xs1428

(set-goal (pf "all xs^(STotal xs^ -> P xs^)"))
(ind)
; ok, ?_1 can be obtained from
; ?_3: all x^1399,xs^1400(
;       STotal xs^1400 -> P xs^1400 -> P((Cons alpha)x^1399 xs^1400)) from
;   xs^1394  1:STotal xs^1394

; ?_2: P(Nil alpha) from
;   xs^1394  1:STotal xs^1394

(set-goal (pf "all xs^(STotal xs^ -> P xs^)"))
(ind)
; ?_1: all xs^(STotal xs^ -> P xs^)
; ok, ?_1 can be obtained from
; ?_3: all x^1392,xs^1393(
;       STotal xs^1393 -> P xs^1393 -> P((Cons alpha)x^1392 xs^1393)) from
;   xs^1387  1:STotal xs^1387

; ?_2: P(Nil alpha) from
;   xs^1387  1:STotal xs^1387

(remove-pvar-name "P")
(remove-var-name "x" "xs")


; Tests for simind

(add-algs (list "tree" "tlist")
	  '("Leaf" "tree")
	  '("Branch" "tlist=>tree")
	  '("Empty" "tlist")
	  '("Tcons" "tree=>tlist=>tlist"))

(add-pvar-name "P" (make-arity (py "tree")))
(add-pvar-name "Q" (make-arity (py "tlist")))

(set-goal (pf "all tree P tree"))
(simind (pf "all tlist Q tlist"))
; ok, ?_1 can be obtained from
; ?_5: all tree55,tlist54.P tree55 -> Q tlist54 -> Q(Tcons tree55 tlist54) from
;   tree51

; ?_4: Q Empty from
;   tree51

; ?_3: all tlist56.Q tlist56 -> P(Branch tlist56) from
;   tree51

; ?_2: P Leaf from
;   tree51

(set-goal (pf "all tree^(STotal tree^ -> P tree^)"))
(simind (pf "all tlist^(STotal tlist^ -> Q tlist^)"))

(remove-pvar-name "P")
(remove-pvar-name "Q")
(remove-alg-name "tree")

(add-algs (list "inftree" "inftlist")
	  '("Newleaf" "boole=>inftree")
          '("Infbranch" "boole=>inftlist=>inftree")
          '("Lim" "boole=>(boole=>inftree)=>inftree")
          '("Emptyinftlist" "inftlist")
          '("Inftcons" "inftree=>inftlist=>inftlist"))

(add-pvar-name "P" (make-arity (py "inftree")))
(add-pvar-name "Q" (make-arity (py "inftlist")))

(set-goal (pf "all inftree P inftree"))
(simind (pf "all inftlist Q inftlist"))

(set-goal (pf "all inftree^(STotal inftree^ -> P inftree^)"))
(simind (pf "all inftlist^(STotal inftlist^ -> Q inftlist^)"))
; ok, ?_1 can be obtained from
; ?_6: all inftree^91,inftlist^90(
;       STotal inftree^91 -> 
;       STotal inftlist^90 -> 
;       P inftree^91 -> Q inftlist^90 -> Q(Inftcons inftree^91 inftlist^90)) from
;   inftree^87  1:STotal inftree^87

; ?_5: Q Emptyinftlist from
;   inftree^87  1:STotal inftree^87

; ?_4: all boole^93,(boole=>inftree)^92(
;       STotal boole^93 -> 
;       all boole94 STotal((boole=>inftree)^92 boole94) -> 
;       all boole95 P((boole=>inftree)^92 boole95) -> 
;       P(Lim boole^93(boole=>inftree)^92)) from
;   inftree^87  1:STotal inftree^87

; ?_3: all boole^97,inftlist^96(
;       STotal boole^97 -> 
;       STotal inftlist^96 -> 
;       Q inftlist^96 -> P(Infbranch boole^97 inftlist^96)) from
;   inftree^87  1:STotal inftree^87

; ?_2: all boole^98(STotal boole^98 -> P(Newleaf boole^98)) from
;   inftree^87  1:STotal inftree^87

(remove-pvar-name "P" "Q")
(remove-alg-name "inftree")


; Tests for cases

(add-pvar-name "P" (make-arity (py "nat")))

(set-goal (pf "all n P n"))
(cases)
; ok, ?_1 can be obtained from
; ?_3: all n1358 P(Succ n1358) from
;   n1356

; ?_2: P 0 from
;   n1356

(set-goal (pf "all n^(STotal n^ -> P n^)"))
(cases)
; ok, ?_1 can be obtained from
; ?_3: all n1370 P(Succ n1370) from
;   n^1368  1:STotal n^1368

; ?_2: P 0 from
;   n^1368  1:STotal n^1368

(set-goal (pf "all n^ P n^"))
(assume "n^")
(cases (pt "n^"))
; ok, ?_2 can be obtained from
; ?_5: all n1376(Equal n^(Succ n1376) -> P(Succ n1376)) from
;   n^

; ?_4: Equal n^ 0 -> P 0 from
;   n^

; ?_3: STotal n^ from
;   n^

(remove-pvar-name "P")

(add-alg "ordl" '("OrdZero" "ordl") '("OrdSup" "(nat=>ordl)=>ordl"))
(add-pvar-name "P" (make-arity (py "ordl")))

(set-goal (pf "all ordl P ordl"))
(cases)
; ok, ?_1 can be obtained from
; ?_3: all (nat=>ordl)_1379 P(OrdSup(nat=>ordl)_1379) from
;   ordl1377

; ?_2: P OrdZero from
;   ordl1377

; (set-goal (pf "all ordl^(STotal ordl^ -> P ordl^)"))
; (cases)
; sfinalg-to-se-const
; structure finitary algebra expected
; ordl

(remove-pvar-name "P")
(remove-alg-name "ordl")

; (add-param-alg "list" 'prefix-typeop
; 	       '("Nil" "list")
; 	       '("Cons" "alpha1=>list=>list"))
(add-pvar-name "P" (make-arity (py "list nat")))
(add-var-name "ns" (py "list nat"))

(set-goal (pf "all ns P ns"))
(cases)
; ok, ?_1 can be obtained from
; ?_3: all n1386,ns1387 P((Cons nat)n1386 ns1387) from
;   ns1381

; ?_2: P(Nil nat) from
;   ns1381

(set-goal (pf "all ns^(STotal ns^ -> P ns^)"))
(cases)

; ok, ?_1 can be obtained from
; ?_3: all n^1400,ns^1401(STotal ns^1401 -> P((Cons nat)n^1400 ns^1401)) from
;   ns^1395  1:STotal ns^1395

; ?_2: P(Nil nat) from
;   ns^1395  1:STotal ns^1395

(set-goal (pf "all ns^ P ns^"))
(assume "ns^")
(cases (pt "ns^"))
; ok, ?_2 can be obtained from
; ?_5: all n^1417,ns^1418(
;       STotal ns^1418 -> 
;       Equal ns^((Cons nat)n^1417 ns^1418) -> P((Cons nat)n^1417 ns^1418)) from
;   ns^

; ?_4: Equal ns^(Nil nat) -> P(Nil nat) from
;   ns^

; ?_3: STotal ns^ from
;   ns^

(remove-pvar-name "P")
(remove-var-name "ns")

(add-pvar-name "P" (make-arity (py "list alpha")))
(add-var-name "x" (py "alpha"))
(add-var-name "xs" (py "list alpha"))

(set-goal (pf "all xs P xs"))
(cases)
; ok, ?_1 can be obtained from
; ?_3: all x1424,xs1425 P((Cons alpha)x1424 xs1425) from
;   xs1419

; ?_2: P(Nil alpha) from
;   xs1419

(set-goal (pf "all xs^(STotal xs^ -> P xs^)"))
(cases)
; ok, ?_1 can be obtained from
; ?_3: all x^1431,xs^1432(STotal xs^1432 -> P((Cons alpha)x^1431 xs^1432)) from
;   xs^1426  1:STotal xs^1426

; ?_2: P(Nil alpha) from
;   xs^1426  1:STotal xs^1426

(set-goal (pf "all xs^(STotal xs^ -> P xs^)"))
(cases)

(remove-pvar-name "P")
(remove-var-name "x" "xs")
; (remove-alg-name "list")

(set-goal (pf "all boole^(STotal boole^ -> boole^ =boole^)"))
(cases)
; ok, ?_1 can be obtained from
; ?_3: False=False from
;   boole^1536  1:STotal boole^1536

; ?_2: True=True from
;   boole^1536  1:STotal boole^1536
(use "Truth-Axiom")
(use "Truth-Axiom")
; Proof finished.

(set-goal (pf "all boole^ boole^ =boole^"))
(assume "boole^")
(cases (pt "boole^"))
; ok, ?_2 can be obtained from
; ?_5: (boole^ -> F) -> False=False from
;   boole^

; ?_4: boole^ -> True=True from
;   boole^

; ?_3: STotal boole^ from
;   boole^


; Test for elim

(add-ids (list (list "Even" (make-arity (py "nat")) "algEven"))
	 '("Even 0" "InitEven")
	 '("allnc n^(Even n^ -> Even(n^ +2))" "GenEven"))

(set-goal (pf "allnc n^(Even n^ -> ex m n^ =m+m)"))
(assume "n^")
(elim)
(ex-intro (pt "0"))
(use "Truth-Axiom")
(assume "n^1" "Even n^1" "IH")
(by-assume-with "IH" "m" "n^1=m+m")
(ex-intro (pt "m+1"))
(ng)
(use "n^1=m+m")
; Proof finished.

(define eterm (proof-to-extracted-term (current-proof)))
(define neterm (nt eterm))
(pp neterm)
; [algEven0](Rec algEven=>nat)algEven0 0([algEven1]Succ)

(remove-idpc-name "Even")

; Test for elim with a simultaneous inductive definition.

(add-ids (list (list "Ev" (make-arity (py "nat")) "algEv")
	       (list "Od" (make-arity (py "nat")) "algOd"))
	 '("Ev 0" "InitEv")
	 '("allnc n^(Od n^ -> Ev(n^ +1))" "GenEv")
	 '("allnc n^(Ev n^ -> Od(n^ +1))" "GenOd"))

(set-goal (pf "allnc n^(Ev n^ -> ex m n^ =m+m)"))
(assume "n^")
(elim (pf "Od n^ -> ex m n^ =m+m+1"))
; ok, ?_2 can be obtained from
; ?_5: allnc n^(Ev n^ -> ex m n^ =m+m -> ex m n^ +1=m+m+1) from
;   {n^}  1:Ev n^

; ?_4: allnc n^(Od n^ -> ex m n^ =m+m+1 -> ex m n^ +1=m+m) from
;   {n^}  1:Ev n^

; ?_3: ex m 0=m+m from
;   {n^}  1:Ev n^

(ex-intro (pt "0"))
(use "Truth-Axiom")

(assume "n^1" "Od n^1" "H1")
(by-assume-with "H1" "m" "H2")
(ex-intro (pt "Succ m"))
(use-with "H2")

(assume "n^1" "Ev n^1" "H1")
(by-assume-with "H1" "m" "H2")
(ex-intro (pt "m"))
(use-with "H2")
; Proof finished.

(define eterm (proof-to-extracted-term (current-proof)))
(define neterm (nt eterm))
(pp neterm)
; [algEv0](Rec algEv=>nat algOd=>nat)algEv0 0([algOd1]Succ)([algEv1,n2]n2)

(remove-idpc-name "Ev")


; Tests for EqD as a uniform one-clause defined idpredconst

(add-var-name "x" "y" "z" (py "alpha"))
(add-pvar-name "Q" (make-arity (py "alpha")))

; In ets.scm:
; (add-ids (list (list "EqD" (make-arity (py "alpha") (py "alpha"))))
; 	 '("allnc x^ EqD x^ x^" "InitEqD"))

; "EqDRefl"
(set-goal (pf "all x^ x^ eqd x^"))
(assume "x^")
(use "InitEqD")
; Proof finished.
(save "EqDRefl")

(set-goal (pf "all x^,y^(x^ eqd y^ -> Q x^ -> Q y^)"))
(assume "x^" "y^")
(elim)
(assume "x^1" "H1")
(use "H1")
; Proof finished.
; (save "EqDCompat")
; EqDCompat
; already is a theorem constant for
; allnc alpha^1,alpha^2(alpha^1 eqd alpha^2 --> (Pvar alpha)alpha^1 -> (Pvar alpha)alpha^2)

; "EqDSym"
(set-goal (pf "all x^,y^(x^ eqd y^ -> y^ eqd x^)"))
(assume "x^" "y^" "H1")
(use-with "EqDCompat"
	  (make-cterm (pv "x^1") (pf "x^1 eqd x^"))
	  (pt "x^") (pt "y^") "?" "?")
(use "H1")
(use "InitEqD")
; Proof finished.
(save "EqDSym")

; "EqDTrans"
(set-goal (pf "all x^,y^,z^(x^ eqd y^ -> y^ eqd z^ -> x^ eqd z^)"))
(assume "x^" "y^" "z^" "H1")
(use-with "EqDCompat"
	  (make-cterm (pv "x^1") (pf "x^1 eqd z^ -> x^ eqd z^"))
	  (pt "x^") (pt "y^") "?" "?")
(use "H1")
(assume "H2")
(use "H2")
; Proof finished.
(save "EqDTrans")

; Use of (pf "False eqd True") for falsity:

(set-goal (pf "all x^,y^(False eqd True -> x^ eqd y^)"))
(assume "x^" "y^" "FF")
(use-with "EqDCompat"
	  (py "boole")
	  (make-cterm (pv "boole^")
		      (pf "[if boole^ x^ y^]eqd[if False x^ y^]"))
	  (pt "False") (pt "True") "?" "?")
(use "FF")
(use "EqDRefl")
; Proof finished.
(save "EFEdD")

(remove-var-name "x" "y" "z")
(remove-pvar-name "Q")


; Test for inversion

(add-ids (list (list "Even" (make-arity (py "nat")) "algEven"))
	 '("Even 0" "InitEven")
	 '("allnc n^(Even n^ -> Even(n^ +2))" "GenEven"))

(set-goal (pf "all n(Even(Succ(Succ n)) -> Even n)"))
(assume "n" "H")
(inversion "H")
(assume "m^")
(ng)
(assume "Even m^" "H1" "n=m^")
(simp "n=m^")
(use "Even m^")
; Proof finished.
; (cdp)

(remove-idpc-name "Even")

; Test for inversion for a simultaneous inductive definition.
; Context: Tait's normalization proof.  Substitutions in
; Hancock/Joachimski style, with a trailing number.  Inductive
; definition of "WN", simultaneously with "WNs".

; (load "~/minlog/init.scm")

(set! COMMENT-FLAG #f)
; (libload "nat.scm")
(libload "list.scm")
(set! COMMENT-FLAG #t)

(add-var-name "l" (py "nat"))

(add-alg "type"
	 '("Iota" "type")
	 '("Arrow" "type=>type=>type"))

(add-token
 "to"
 'pair-op
 (lambda (x y)
   (let* ((type1 (term-to-type x))
	  (type2 (term-to-type y))
	  (type (types-lub type1 type2)))
     (mk-term-in-app-form
      (make-term-in-const-form (constr-name-to-constr "Arrow"))
      x y))))

(add-display
 (py "type")
 (lambda (x)
   (let ((op (term-in-app-form-to-final-op x))
	 (args (term-in-app-form-to-args x)))
     (if (and (term-in-const-form? op)
	      (string=? "Arrow"
			(const-to-name (term-in-const-form-to-const op)))
	      (= 2 (length args)))
	 (list 'pair-op "to"
	       (term-to-token-tree (car args))
	       (term-to-token-tree (cadr args)))
	 #f))))

(add-var-name "rho" "sig" "tau" (py "type"))

(add-program-constant "Argtyp" (py "type=>type") 1)
(add-program-constant "Valtyp" (py "type=>type") 1)
(add-program-constant "Arrowtyp" (py "type=>boole") 1)

(add-computation-rule (pt "Argtyp Iota") (pt "Iota"))
(add-computation-rule (pt "Valtyp Iota") (pt "Iota"))
(add-computation-rule (pt "Argtyp(rho to sig)") (pt "rho"))
(add-computation-rule (pt "Valtyp(rho to sig)") (pt "sig"))

(add-computation-rule (pt "Arrowtyp Iota") (pt "False"))
(add-computation-rule (pt "Arrowtyp(rho to sig)") (pt "True"))

(add-alg "term"
	 '("Var" "nat=>term")
	 '("App" "term=>term=>term")
	 '("Abs" "type=>term=>term"))

; Application for terms is via the constant App

(add-new-application 
 (lambda (type) (equal? type (py "term")))
 (lambda (term1 term2) (mk-term-in-app-form (pt "App") term1 term2)))

(add-new-application-syntax
 ; predicate
 (lambda (term)
   (and (term-in-app-form? term)
	(let ((op (term-in-app-form-to-op term)))
	  (term-in-app-form? op)
	  (term=? (pt "App") (term-in-app-form-to-op op)))))
 ; to arg
 (lambda (term)
   (term-in-app-form-to-arg term))
 ; to op
 (lambda (term)
   (term-in-app-form-to-arg
    (term-in-app-form-to-op term))))

(add-var-name "r" "s" "t" (py "term"))
(add-var-name "rs" "ss" "ts" (py "list term"))
(add-var-name "rhos" "sigs" "taus" (py "list type")) ;used for contexts

(add-program-constant "Typ" (py "list type=>term=>type") 1)

(add-computation-rule (pt "Typ(Nil type)(Var n)") (pt "Iota"))
(add-computation-rule (pt "Typ(rho::rhos)(Var 0)") (pt "rho"))
(add-computation-rule (pt "Typ(rho::rhos)(Var(Succ n))")
		      (pt "Typ rhos(Var n)"))
(add-computation-rule (pt "Typ rhos(r s)") (pt "Valtyp(Typ rhos r)"))
(add-computation-rule (pt "Typ rhos(Abs rho r)")
		      (pt "rho to Typ(rho::rhos)r"))

(add-program-constant "Cor" (py "list type=>term=>boole") 1)

(add-computation-rule (pt "Cor rhos(Var n)") (pt "n<Lh rhos"))
(add-computation-rule (pt "Cor rhos(r s)")
		      (pt "Cor rhos r and Cor rhos s and
                           Typ rhos r=(Typ rhos s to Valtyp(Typ rhos r))"))
(add-computation-rule (pt "Cor rhos(Abs rho r)") (pt "Cor(rho::rhos)r"))

(add-program-constant "Lift" (py "term=>nat=>nat=>term") 1)

(add-computation-rule (pt "Lift(Var n)l k")
		      (pt "[if (n<l) (Var n) (Var(n+k))]"))
(add-computation-rule (pt "Lift(r s)l k")
		      (pt "(Lift r l k)(Lift s l k)"))
(add-computation-rule (pt "Lift(Abs rho r)l k")
		      (pt "Abs rho(Lift r(l+1)k)"))

; Substitution in the style of Hancock/Joachimski

(add-alg "sub"
	 '("Up" "nat=>sub")
	 '("Dot" "term=>sub=>sub"))

(add-var-name "theta" (py "sub"))

(add-program-constant "Sublift" (py "sub=>nat=>sub") 1)

(add-computation-rule (pt "Sublift(Up m)n") (pt "Up(m+n)"))
(add-computation-rule (pt "Sublift(Dot r theta)n")
		      (pt "Dot(Lift r 0 n)(Sublift theta n)"))

; For convenience we want to view a substitution as a pair of a list
; and a number.

(add-program-constant "Mksub" (py "list term=>nat=>sub") 1)

(add-computation-rule (pt "Mksub(Nil term)n") (pt "Up n"))
(add-computation-rule (pt "Mksub(r::rs)n") (pt "Dot r(Mksub rs n)"))

(add-program-constant "Sublist" (py "sub=>list term") 1)

(add-computation-rule (pt "Sublist(Up n)") (pt "(Nil term)"))
(add-computation-rule (pt "Sublist(Dot r theta)") (pt "r::(Sublist theta)"))

(add-program-constant "Subup" (py "sub=>nat") 1)

(add-computation-rule (pt "Subup(Up n)") (pt "n"))
(add-computation-rule (pt "Subup(Dot r theta)") (pt "Subup theta"))


; Sub r theta substitutes theta in the term r

(add-program-constant "Sub" (py "term=>sub=>term") 1)

(add-computation-rule (pt "Sub(Var n)(Up m)") (pt "Var(n+m)"))
(add-computation-rule (pt "Sub(Var 0)(Dot r theta)") (pt "r"))
(add-computation-rule (pt "Sub(Var(Succ n))(Dot r theta)")
		      (pt "Sub(Var n)theta"))
(add-computation-rule (pt "Sub(r s)theta") (pt "(Sub r theta)(Sub s theta)"))
(add-computation-rule (pt "Sub(Abs rho r)theta")
		      (pt "(Abs rho(Sub r(Dot(Var 0)(Sublift theta 1))))"))


; Wrap n rs wraps up a list of terms to a Sublist with a parameter for lifting

(add-program-constant "Wrap" (py "nat=>list term=>sub") 1)

(add-computation-rule (pt "Wrap n(Nil term)") (pt "Up n"))
(add-computation-rule (pt "Wrap n(r::rs)") (pt "Dot r(Wrap n rs)"))


; Eta is the outer eta expansion
(add-program-constant "Eta" (py "type=>term=>term") 1)

(add-computation-rule (pt "Eta Iota r") (pt "r"))
(add-computation-rule (pt "Eta(rho to sig)r") 
		      (pt "Abs rho(Eta sig(Lift r 0 1(Eta rho(Var 0))))"))

(pp (nt (pt "Eta(Iota to Iota)(Var 0)")))
(pp (nt (pt "Eta(Iota to Iota)(Var 7)")))
(pp (nt (pt "Eta((Iota to Iota)to(Iota to Iota))(Var 7)")))

; Notice that the "1" (i.e., the totality) of Eta must be proved.
; This is easy, by induction on types.


; Exp is full eta expansion.  It is defined simultaneously with IExp,
; the inner eta expansion.

(add-program-constant "Exp" (py "list type=>type=>term=>term") 1)
(add-program-constant "IExp" (py "list type=>term=>term") 1)

(add-computation-rule (pt "Exp rhos rho(Var n)") (pt "Eta rho(Var n)"))
(add-computation-rule (pt "Exp rhos rho(r s)")
		      (pt "Eta rho(IExp rhos(r s))"))
(add-computation-rule (pt "Exp rhos tau(Abs rho r)")
		      (pt "Abs rho(Exp(rho::rhos)(Valtyp tau)r)"))

(add-computation-rule (pt "IExp rhos(Var n)") (pt "Var n"))
(add-computation-rule (pt "IExp rhos(r s)")
		      (pt "IExp rhos r(Exp rhos(Typ rhos s)s)"))

; Notice that the "1" (i.e., the totality) of Exp and IExp must be
; proved.  This is easy, by induction on terms (simultaneously).

(pp (pt "Abs rho(Abs sig(Var 1))")) ;K
(pp (pt "Abs(rho to sig to rho)
          (Abs(rho to sig)
            (Abs rho(Var 2(Var 0)(Var 1(Var 0)))))")) ;S

(define sterm
  (pt "Abs((Iota to Iota) to Iota to (Iota to Iota))
          (Abs((Iota to Iota) to Iota)
            (Abs (Iota to Iota)(Var 2(Var 0)(Var 1(Var 0)))))"))
(define stype (mk-term-in-app-form (pt "Typ") (pt "(Nil type)") sterm))
(pp stype)
(pp (nt stype))

(pp (nt (mk-term-in-app-form (pt "Exp(Nil type)") stype sterm)))


(add-program-constant "FoldApp" (py "term => list term => term") 1)

(add-computation-rule (pt "FoldApp r(Nil term)") (pt "r"))
(add-computation-rule (pt "FoldApp r(s::ss)") (pt "FoldApp(r s)ss"))

; (pp (nt (pt "FoldApp r(s::t:)")))
; => r s t


; Inductive definition of "WN", simultaneously with "WNs".

(add-ids
 (list (list "WN" (make-arity (py "term") (py "term")) "algWN")
       (list "WNs" (make-arity (py "list term") (py "list term")) "algWNs"))
 '("all n,rs,ss(WNs rs ss -> WN(FoldApp(Var n)rs)(FoldApp(Var n)ss))" "WNVar")
 '("all rho,r,s(WN r s -> WN(Abs rho r)(Abs rho s))" "WNAbs")
 '("all rho,r,s,t,rs(WN(FoldApp(Sub r(Wrap 0(s:)))rs)t ->
     WN(FoldApp(Abs rho r)(s::rs))t)" "WNBeta")
 '("WNs(Nil term)(Nil term)" "WNsNil")
 '("all r,s,rs,ss(WN r s -> WNs rs ss -> WNs(r::rs)(s::ss))" "WNsCons"))

(set-goal (pf "all r,s,rs,ss(WNs(r::rs)(s::ss) -> WNs rs ss)"))
(assume "r" "s" "rs" "ss" "WNs(r::rs)(s::ss)")
(simplified-inversion "WNs(r::rs)(s::ss)")
(assume "r1" "s1" "rs1" "ss1")
(assume "WNs rs1 ss1" "H1" "(r::rs)=(r1::rs1)" "(s::ss)=(s1::ss1)")
(ng)
(inst-with-to "(r::rs)=(r1::rs1)" 'right "rs=rs1")
(simp "rs=rs1")
(inst-with-to "(s::ss)=(s1::ss1)" 'right "ss=ss1")
(simp "ss=ss1")
(use "WNs rs1 ss1")
; Proof finished.
; (cdp)
; (cdp (np (current-proof)))

(define eterm (proof-to-extracted-term (current-proof)))
(pp eterm)

; [r,s,rs,ss,algWNs2528]
;  (Rec algWNs=>algWNs)algWNs2528 cWNsNil
;  ([r1,s1,rs1,ss1,algWNs2535,algWNs2536]
;    ([algWNs2531]algWNs2531)(([algWNs2534]algWNs2534)algWNs2535))


(set-goal (pf "all r,rs,ss(WNs(r::rs)ss -> ss=(Nil term) -> F)"))
(assume "r" "rs" "ss" "H1")
(simplified-inversion "H1")
(assume "r1" "s1" "rs1" "ss1" "H2" "H3" "H4" "H5")
(simp "H5")
(prop)
; Proof finished.
; (cdp)
; (cdp (np (current-proof)))

; WNTest0
(set-goal (pf "all rs,ss(WNs rs ss -> rs=(Nil term) -> ss=(Nil term))"))
(assume "rs" "ss")
(elim)
(prop)
(strip)
(prop)
; Proof finished.
; (cdp)

; WNsNil
(set-goal (pf "all ss(WNs(Nil term)ss -> ss=(Nil term))"))
(assume "ss" "H1")
(simplified-inversion "H1")
(prop)
; Proof finished.
; (cdp)
; (cdp (np (current-proof)))


; "WNsApp"
(set-goal (pf "all rs1,ss1,rs2,ss2(
                WNs rs1 ss1 -> WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))"))
(ind)
(cases)

(strip)
(ng)
(use 2)

(strip)
(simplified-inversion 1)

(assume "r1" "rs1" "IH")
(cases)
(strip)
(simplified-inversion 2)

(assume "s1" "ss1" "rs2" "ss2" "H")
(inversion "H")
(assume "r" "s" "rs" "ss")
(strip)
(ng)
(inst-with-to 7 'left "r1=r")
(simp "r1=r")
(inst-with-to 8 'left "s1=s")
(simp "s1=s")
(use "WNsCons")
(use 5)
(use "IH")
(inst-with-to 7 'right "rs1=rs")
(simp "rs1=rs")
(inst-with-to 8 'right "ss1=ss")
(simp "ss1=ss")
(use 4)
(use 9)
; Proof finished
; (save "WNsApp")
; (cdp)
; (cdp (np (current-proof)))

; Inductive definition of "H" meaning "has a head normal form"

(add-ids
 (list (list "H" (make-arity (py "term")) "algH"))
 '("all n,rs H(FoldApp(Var n)rs)" "HVar")
 '("all rho,r(H r -> H(Abs rho r))" "HAbs")
 '("all rho,r,s,rs(H(FoldApp(Sub r(Wrap 0(s:)))rs) ->
     H(FoldApp(Abs rho r)(s::rs)))" "HBeta"))

(set-goal (pf "all r,s(WN r s -> H r)"))
(assume "r" "s")
(elim)
(strip)
(use "HVar")
(strip)
(use "HAbs")
(use 3)
(strip)
(use "HBeta")
(use 3)
; Proof finished.
; (cdp)
; (cdp (np (current-proof)))

(define eterm (proof-to-extracted-term (current-proof)))
(define neterm (nt eterm))
(pp neterm)
; [r0,r1,algWN2]
;  (Rec algWN=>algH)algWN2([n3,rs4,rs5]cHVar n3 rs4)
;  ([rho3,r4,r5,algWN6]cHAbs rho3 r4)
;  ([rho3,r4,r5,r6,rs7,algWN8]cHBeta rho3 r4 r5 rs7)

(remove-var-name "l" "rho" "sig" "tau"
		 "r" "s" "t"
		 "rs" "ss" "ts"
		 "rhos" "sigs" "taus"
		 "theta")

(remove-alg-name "type" "sub")
(remove-idpc-name "H")
(remove-idpc-name "WN")

; Tests for search

(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))
(add-pvar-name "Q" (make-arity (py "alpha")))
(add-pvar-name "P" (make-arity))
(add-var-name "x" "y" "z" (py "alpha"))

; (set! VERBOSE-SEARCH #t)

(set-goal (pf "all y(all z R y z -> P) -> all y1,y2 R y1 y2 -> P"))
(search)

(proof-to-expr (current-proof))

; (lambda (u67) (lambda (u68) ((u67 y) (lambda (z) ((u68 y) z)))))
; Contains y free.


; "Drinker"
(set-goal (pf "all y(((Q y -> F) -> F) -> Q y) -> exca x(Q x -> all y Q y)"))
(assume "StabQ" "FHyp")
(use "FHyp" (pt "(Inhab alpha)"))
(assume "QInhab" "y")
(use "StabQ")
(assume "NotQy")
(use "FHyp" (pt "y"))
(assume "Qy" "z")
(use "StabQ")
(assume "NotQz")
(use "NotQy")
(use "Qy")
; Proof finished.

(proof-to-expr (current-proof))

; (lambda (|StabQ111|)
;   (lambda (|FHyp112|)
;     ((|FHyp112| |Inhab|)
;       (lambda (|QInhab114|)
;         (lambda (y)
;           ((|StabQ111| y)
;             (lambda (|NotQy116|)
;               ((|FHyp112| y)
;                 (lambda (|Qy118|)
;                   (lambda (z)
;                     ((|StabQ111| z)
;                       (lambda (|NotQz120|) (|NotQy116| |Qy118|)))))))))))))

(set-goal (pf "all y(((Q y -> F) -> F) -> Q y) -> exca x(Q x -> all y Q y)"))
(search)
; Proof finished.

(proof-to-expr (current-proof))

; (lambda (u102)
;   (lambda (u103)
;     ((u103 x)
;       (lambda (u104)
;         (lambda (y)
;           ((u102 y)
;             (lambda (u105)
;               ((u103 y)
;                 (lambda (u108)
;                   (lambda (y92)
;                     ((u102 y92) (lambda (u109) (u105 u108)))))))))))))

; Contains y free.

(remove-var-name "x" "y" "z")
(remove-pvar-name "P" "Q" "R")


; 13. Automated propositional proofs
; ==================================
; (prop.scm)


; 16. Extracted terms
; ===================
; (ets.scm and etsd.scm)

; Tests for extraction with realizability and Dialectica
; Based on Trifon Trifonov's /dialectica/minlog/etsd-test.scm.

(define (extraction-test-et proof)
  (extraction-test-aux proof proof-to-extracted-term))

(define (extraction-test-etd proof)
  (extraction-test-aux proof proof-to-extracted-d-term))

(define (extraction-test-aux proof extract)
  (let ((et (extract proof)))
    (if (eq? 'eps et)
	(display 'eps)
	(begin
	  (pp et)
	  (newline)
	  (pp (nt et))))
    (newline)))

(define (extraction-test proof)
  (extraction-test-et proof)
  (extraction-test-etd proof))

;----------------------------------------------------------------------
; simple proof by cases
;----------------------------------------------------------------------

(set-goal (pf "all n1 ex n2 all n3(n1=n3 -> n2=n3)"))
(cases)
(ex-intro (pt "0"))
(assume "n" "u")
(use "u")
(assume "n1")
(strip)
(ex-intro (pt "Succ n1"))
(assume "n" "u")
(use "u")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; simple proof by induction
;----------------------------------------------------------------------

(set-goal (pf "all n1 ex n2 all n3(n1=n3 -> n2=n3)"))
(ind)
(ex-intro (pt "0"))
(assume "n" "u")
(use "u")
(assume "n1")
(strip)
(ex-intro (pt "Succ n1"))
(assume "n" "u")
(use "u")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; simple proof by general induction
;----------------------------------------------------------------------

(set-goal (pf "all n1 ex n2 all n3(n1=n3 -> n2=n3)"))
(gind (pt "[n]n"))
(assume "n1")
(strip)
(ex-intro (pt "n1"))
(assume "n" "u")
(use "u")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; proof by induction in which the IH is used
;----------------------------------------------------------------------

(set-goal (pf "all n1 ex n2 all n3(n1<n3 -> n2<=n3)"))
(ind)
; base case
(ex-intro (pt "1"))
(cases)
; base subcase
(assume "u")
(use "u")
; step subcase
(assume "n3" "u")
(use "u")
; step case
(assume "n1" "IH")
(by-assume-with "IH" "n2" "v")
(ex-intro (pt "Succ n2"))
(cases)
; base subcase
(assume "u")
(use "u")
; step subcase
(assume "n3" "u")
(use "v")
(use "u")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; proof by induction with a relevant assumption for Dialectica
;----------------------------------------------------------------------

(set-goal
 (pf "all n1,n2(all n3(n1<n3 -> n2<=n3) ->
                all n3(Succ n1<n3 -> Succ n2<=n3)) -> 
      all n1 ex n2 all n3(n1<n3 -> n2<=n3)"))
(assume "L")
(ind)
; base case
(ex-intro (pt "1"))
(cases)
; base subcase
(assume "u")
(use "u")
; step subcase
(assume "n3" "u")
(use "u")
; step case
(assume "n1" "IH")
(by-assume-with "IH" "n2" "v")
(ex-intro (pt "Succ n2"))
(use "L")
(use "v")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; list induction
;----------------------------------------------------------------------

(set! COMMENT-FLAG #f)
(libload "list.scm")
(set! COMMENT-FLAG #t)

(add-var-name "ns" (py "list nat"))

;----------------------------------------------------------------------
; simple proof by list induction
;----------------------------------------------------------------------

(set-goal (pf "all ns1 ex ns2 all ns3(ns1=ns3 -> ns2=ns3)"))
(ind)
(ex-intro (pt "(Nil nat)"))
(assume "ns" "u")
(use "u")
(assume "n" "ns1")
(strip)
(ex-intro (pt "n::ns1"))
(assume "ns" "u")
(use "u")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; proof by list induction in which the IH is used
;----------------------------------------------------------------------
(set-goal (pf "all ns1 ex ns2 all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)"))
(ind)
; base case
(ex-intro (pt "0:"))
(cases)
; base subcase
(assume "u")
(use "u")
; step subcase
(assume "n3" "ns3" "u")
(use "u")
; step case
(assume "n1" "ns1" "IH")
(by-assume-with "IH" "ns2" "v")
(ex-intro (pt "0::ns2"))
(cases)
; base subcase
(assume "u")
(use "u")
; step subcase
(assume "n3" "ns3" "u")
(use "v")
(use "u")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; proof by list induction with a relevant assumption for Dialectica
;----------------------------------------------------------------------

(set-goal
 (pf "all ns1,n1,ns2(
       all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
       all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3)) -> 
       all ns1 ex ns2 all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)"))
(assume "L")
(ind)
; base case
(ex-intro (pt "0:"))
(cases)
; base subcase
(assume "u")
(use "u")
; step subcase
(assume "n3" "ns3" "u")
(use "u")
; step case
(assume "n1" "ns1" "IH")
(by-assume-with "IH" "ns2" "v")
(ex-intro (pt "n1::ns2"))
(use "L" (pt "n1"))
(use "v")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; proof by cases using predicate variables
;----------------------------------------------------------------------

(add-pvar-name "R" (make-arity (py "nat") (py "nat")))

(set-goal
 (pf "R 0 1 -> all n1 ex n2 R(Succ n1)(Succ n2) -> all n1 ex n2 R n1 n2"))
(assume "Base" "Step")
(cases)
(ex-intro (pt "1"))
(use "Base")
(assume "n1")
(inst-with-to "Step" (pt "n1") "Step1")
(by-assume-with "Step1" "n2" "Step2")
(ex-intro (pt "Succ n2"))
(use "Step2")
(extraction-test (current-proof))

; (proof-to-expr (current-proof))
; (proof-to-expr (np (current-proof)))

(set-goal
 (pf "R^ 0 1 -> all n1 ex n2 R^(Succ n1)(Succ n2) -> all n1 ex n2 R^ n1 n2"))
(assume "Base" "Step")
(cases)
(ex-intro (pt "1"))
(use "Base")
(assume "n1")
(inst-with-to "Step" (pt "n1") "Step1")
(by-assume-with "Step1" "n2" "Step2")
(ex-intro (pt "Succ n2"))
(use "Step2")
(extraction-test (current-proof))

(set-goal
 (pf "R' 0 1 -> all n1 ex n2 R'(Succ n1)(Succ n2) -> all n1 ex n2 R' n1 n2"))
(assume "Base" "Step")
(cases)
(ex-intro (pt "1"))
(use "Base")
(assume "n1")
(inst-with-to "Step" (pt "n1") "Step1")
(by-assume-with "Step1" "n2" "Step2")
(ex-intro (pt "Succ n2"))
(use "Step2")
(extraction-test (current-proof))

(set-goal
 (pf "R^' 0 1 -> 
     all n1 ex n2 R^'(Succ n1)(Succ n2) ->
     all n1 ex n2 R^' n1 n2"))
(assume "Base" "Step")
(cases)
(ex-intro (pt "1"))
(use "Base")
(assume "n1")
(inst-with-to "Step" (pt "n1") "Step1")
(by-assume-with "Step1" "n2" "Step2")
(ex-intro (pt "Succ n2"))
(use "Step2")
(extraction-test (current-proof))

;----------------------------------------------------------------------
; proof by induction using predicate variables
;----------------------------------------------------------------------

(set-goal
 (pf "R 0 1 -> 
      all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2)) -> 
      all n1 ex n2 R n1 n2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "1"))
(use "Base")
(assume "n1" "IH")
(by-assume-with "IH" "n2" "IH1")
(inst-with-to "Step" (pt "n1") "Step1")
(ex-intro (pt "Succ n2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; (extraction-test-etd (current-proof))
; Dialectica gives a contraction error, because of presence of pvars

(set-goal
 (pf "R^' 0 1 -> 
      all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2)) -> 
      all n1 ex n2 R^' n1 n2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "1"))
(use "Base")
(assume "n1" "IH")
(by-assume-with "IH" "n2" "IH1")
(inst-with-to "Step" (pt "n1") "Step1")
(ex-intro (pt "Succ n2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; (extraction-test-etd (current-proof))
; Dialectica gives a contraction error, because of presence of pvars

(set-goal (pf "R^' 0 1 ->
   allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2)) ->
   all n1 ex n2 R^' n1 n2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "1"))
(use "Base")
(assume "n1" "IH")
(by-assume-with "IH" "n2" "IH1")
(inst-with-to "Step" (pt "n1") "Step1")
(ex-intro (pt "Succ n2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; Dialectica not yet properly implemented for allnc.

;----------------------------------------------------------------------
; general induction with predicate variables
;----------------------------------------------------------------------

(set-goal
 (pf "all n1(all n3(n3<n1 -> ex n2 R n3 n2) -> ex n2 R n1 n2) -> 
      all n1 ex n2 R n1 n2"))
(assume "L")
(gind (pt "[n]n"))
(assume "n1" "GIH")
(use "L")
(use "GIH")
(extraction-test-et (current-proof))
; (extraction-test-etd (current-proof))
; Dialectica gives a contraction error, because of presence of pvarsx

(remove-pvar-name "R")

;----------------------------------------------------------------------
; proof by list induction using predicate variables
;----------------------------------------------------------------------

(add-pvar-name "R" (make-arity (py "list nat") (py "list nat")))

(set-goal
 (pf "R(Nil nat)(0:) -> 
      all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2)) -> 
      all ns1 ex ns2 R ns1 ns2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "0:"))
(use "Base")
(assume "n" "ns1" "IH")
(by-assume-with "IH" "ns2" "IH1")
(inst-with-to "Step" (pt "ns1") "Step1")
(ex-intro (pt "n::ns2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; Dialectica gives a contraction error, because of presence of pvars

(set-goal
 (pf "R^'(Nil nat)(0:) -> 
      all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2)) -> 
      all ns1 ex ns2 R^' ns1 ns2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "0:"))
(use "Base")
(assume "n" "ns1" "IH")
(by-assume-with "IH" "ns2" "IH1")
(inst-with-to "Step" (pt "ns1") "Step1")
(ex-intro (pt "n::ns2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; Dialectica gives a contraction error, because of presence of pvars

(set-goal
 (pf "R^'(Nil nat)(0:) -> 
      allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2)) -> 
      all ns1 ex ns2 R^' ns1 ns2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "0:"))
(use "Base")
(assume "n" "ns1" "IH")
(by-assume-with "IH" "ns2" "IH1")
(inst-with-to "Step" (pt "ns1") "Step1")
(ex-intro (pt "n::ns2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; Dialectica not yet properly implemented for allnc.

(remove-pvar-name "R")
(remove-var-name "ns")

;----------------------------------------------------------------------
; proof by list induction on general lists using predicate variables
;----------------------------------------------------------------------

(add-var-name "x" (py "alpha"))
(add-var-name "xs" (py "list alpha"))
(add-pvar-name "R" (make-arity (py "list alpha") (py "list alpha")))

(set-goal
 (pf "R(Nil alpha)(Nil alpha) -> 
      all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2)) -> 
      all xs1 ex xs2 R xs1 xs2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "(Nil alpha)"))
(use "Base")
(assume "x" "xs1" "IH")
(by-assume-with "IH" "xs2" "IH1")
(inst-with-to "Step" (pt "xs1") "Step1")
(ex-intro (pt "x::xs2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; Dialectica gives a contraction error, because of presence of pvars

(set-goal
 (pf "R^'(Nil alpha)(Nil alpha) -> 
      all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2)) -> 
      all xs1 ex xs2 R^' xs1 xs2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "(Nil alpha)"))
(use "Base")
(assume "x" "xs1" "IH")
(by-assume-with "IH" "xs2" "IH1")
(inst-with-to "Step" (pt "xs1") "Step1")
(ex-intro (pt "x::xs2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; Dialectica gives a contraction error, because of presence of pvars

(set-goal
 (pf "R^'(Nil alpha)(Nil alpha) -> 
      allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2)) -> 
      all xs1 ex xs2 R^' xs1 xs2"))
(assume "Base" "Step")
(ind)
(ex-intro (pt "(Nil alpha)"))
(use "Base")
(assume "x" "xs1" "IH")
(by-assume-with "IH" "xs2" "IH1")
(inst-with-to "Step" (pt "xs1") "Step1")
(ex-intro (pt "x::xs2"))
(use "Step1")
(use "IH1")
(extraction-test-et (current-proof))
; Dialectica not yet properly implemented for allnc.

(remove-pvar-name "R")
(remove-var-name "x" "xs")

;----------------------------------------------------------------------
; simple proof by induction using a weak existential
;----------------------------------------------------------------------
(set-goal (pf "all nat1 exca nat2 all nat3(nat1=nat3 -> nat2=nat3)"))
(ind)
(assume "v")
(use "v" (pt "0"))
(assume "n" "u")
(use "u")
(assume "nat1" "IH" "v")
(use "v" (pt "Succ nat1"))
(assume "n" "u")
(use "u")
(extraction-test-etd (current-proof))


; 17. A-translation
; =================
; (atr.scm)