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

(add-var-name "p" (py "nat=>boole"))

(add-program-constant "inf" (py "nat"))
(add-program-constant "Step" (py "unit=>uysum(nat ysum unit)"))
(add-computation-rules "Step unit" "(InrUysum nat ysum unit)((InR unit nat)unit)")
(add-computation-rules "inf" "(CoRec unit=>nat)Dummy Step")
;;(pp (nt (undelay-delayed-corec (pt "(CoRec nat=>nat)Zero ([n](InrUysum nat ysum nat)((InR nat nat) (Succ n)))") 10)))
;;(pp (nt (undelay-delayed-corec (pt "(CoRec unit=>nat)Dummy([unit](InrUysum nat ysum unit)((InR unit nat)unit))") 5)))

;;(add-var-name "Step" (py "unit=>uysum(nat ysum unit)"))

(set-goal "CoTotalNat inf")
(ng #t)
(assert "all n^(exl unit n^ eqd (CoRec unit=>nat)unit Step -> CoTotalNat n^)")
(assume "n^")
(coind)
(assume "m^" "ExHyp")
(intro 1)
(by-assume "ExHyp" "unit" "uProp")
(cases (pt "unit"))
(assume "uEq")
(intro 0 (pt "(CoRec unit=>nat)Dummy Step"))
(split)
(intro 1)
(intro 0 (pt "Dummy"))
(intro 0)
(simphyp-to "uProp" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))) "uPropII")
(simp "uPropII")
(ng #t)
(simp "uEq")
(intro 0)
(assume "AllHyp")
(use "AllHyp")
(intro 0 (pt "Dummy"))
(ng #t)
(intro 0)
(save "infCoTotal")

;; phi (p) = [if (p 0) inl(dummy) else inr (lambda(n) p(succ(n)))}
;; eps (p) = [if (p 0) 0 else succ (eps (lambda(n)(p(succ n))))]

(add-program-constant "phi" (py "(nat=>boole)=>uysum(nat ysum (nat=>boole))"))
(add-computation-rules "phi p" "[if (p Zero) (DummyL nat ysum (nat=>boole)) (Inr((InR (nat=>boole) nat)([n](p (Succ n)))))]")

(add-program-constant "eps" (py "(nat=>boole)=>nat"))
(add-computation-rules "eps p" "(CoRec (nat=>boole)=>nat)p phi")

(set-goal "allnc n^(CoTotalNat n^ -> CoTotalNat (Succ n^))")
(assert "allnc n^,m^(CoTotalNat n^ andl m^ eqd Succ n^ -> CoTotalNat m^)")
(assume "l^0" "l^1")
(coind)
(assume "n^1" "Conj")
(intro 1)
(intro 0 (pt "l^0"))
(split)
(intro 0)
(use "Conj")
(use "Conj")
(assume "Assertion")
(assume "n^" "CoTn")
(use "Assertion" (pt "n^"))
(split)
(use "CoTn")
(use "InitEqD")
(save "NatSuccCoTotal")

(set-goal "allnc n^(Total n^ -> CoTotalNat n^)")
(assume "n^")
(elim)
(assert "all n^(n^ eqd Zero andr Total n^ -> CoTotalNat n^)")
(assume "m^")
(coind)
(assume "n^0" "Hyp")
(intro 0)
(use "Hyp")
(assume "AllHyp")
(use "AllHyp")
(split)
(intro 0)
(intro 0)
(assume "n^0" "Tn0" "CoTn0")
(use "NatSuccCoTotal")
(use "CoTn0")
(save "NatTotalToCoTotal")

(define eterm (proof-to-extracted-term))
(animate "NatSuccCoTotal")
(pp (nt eterm))
;; [n0]
;; (Rec nat=>nat)n0((CoRec nat=>nat)0([n1](DummyL nat ysum nat)))
;; ([n1,n2](CoRec nat=>nat)n2([n3]Inr((InL nat nat)n3)))


;; (assume "n^")
;; (coind)
;; (assume "n^0")
;; (elim)
;; (intro 0)
;; (intro 0)
;; (assume "m^0" "Tm0" "Disj")
;; (elim "Disj")
;; (assume "m0=0")
;; (intro 1)
;; (intro 0 (pt "0"))
;; (split)
;; (intro 1)
;; (intro 0)
;; (simp "m0=0")
;; (intro 0)
;; (assume "ExHyp")
;; (by-assume "ExHyp" "m^1" "m1Prop")
;; (intro 1)
;; (intro 0 (pt "m^0"))
;; (split)
;; (elim "m1Prop")
;; (elim)
;; (assume "CoTm1" "m0Def")
;; (assert "allnc n^,m^(CoTotalNat n^ andl m^ eqd Succ n^ -> CoTotalNat m^)")
;; (assume "l^0" "l^1")
;; (coind)
;; (assume "n^1" "Conj")
;; (intro 1)
;; (intro 0 (pt "l^0"))
;; (split)
;; (intro 0)
;; (use "Conj")
;; (use "Conj")
;; (assume "Assertion")
;; (intro 0)
;; (use "Assertion" (pt "m^1"))
;; (split)
;; (use "CoTm1")
;; (use "m0Def")
;; (assume "Tm1" "m0Def")
;; (intro 1)
;; (simp "m0Def")
;; (intro 1)
;; (use "Tm1")
;; (use "InitEqD")
;; ;;(cdp)
;; (save "NatTotalToCoTotal")

;; (define eterm (proof-to-extracted-term))
;; (pp (nt eterm))

;; [n0]
;; (CoRec nat=>nat)n0
;; ([n1]
;;   (Rec nat=>uysum(nat ysum nat))n1(DummyL nat ysum nat)
;;   ([n2,(uysum(nat ysum nat))_3]
;;     [if (uysum(nat ysum nat))_3
;;       (Inr((InR nat nat)0))
;;       ([(nat ysum nat)_4]
;;        Inr[if (nat ysum nat)_4
;;             ([n5](InL nat nat)((CoRec nat=>nat)n5([n6]Inr((InL nat nat)n6))))
;;             ([n5](InR nat nat)(Succ n5))])]))

(set-goal "allnc n^(CoTotal n^ -> CoEqPNat n^ n^)")
(assert "allnc n^,m^(CoTotal n^ andi n^ eqd m^ -> CoEqPNat n^ m^)")
(assume "n^" "m^")
(coind)
(assume "n^0" "m^0")
(elim)
(assume "CoTn0" "n0=m0")
(inst-with-to "CoTotalNatClause" (pt "n^0") "CoTn0" "Inst")
(elim "Inst")
(assume "n0=0")
(intro 0)
(split)
(use "n0=0")
(simp "<-" "n0=m0")
(use "n0=0")
(assume "ExHyp")
(by-assume "ExHyp" "n^1" "n1Prop")
(elim "n1Prop")
(assume "CoTn1" "n0=Sn1")
(intro 1)
(intro 0 (pt "n^1"))
(intro 0 (pt "n^1"))
(split)
(intro 1)
(split)
(use "CoTn1")
(use "InitEqD")
(split)
(use "n0=Sn1")
(simp "<-" "n0=m0")
(use "n0=Sn1")
(assume "Assertion")
(assume "n^" "CoTn")
(use "Assertion")
(split)
(use "CoTn")
(use "InitEqD")
(save "CoEqPNatRefl")

(set-goal "allnc n^,m^(CoEqPNat n^ m^ -> CoEqPNat (Succ n^) (Succ m^))")
(assert "allnc n^,m^(exr n^0,m^0(n^ eqd Succ n^0 andi m^ eqd Succ m^0 andi CoEqPNat n^0 m^0) -> CoEqPNat n^ m^)")
(assume "n^" "m^")
(coind)
(assume "n^0" "m^0" "ExHyp")
(by-assume "ExHyp" "n^1" "n1Prop")
(by-assume "n1Prop" "m^1" "m1Prop")
(elim "m1Prop")
(assume "n0=Sn1")
(elim)
(assume "m0=Sm1" "n1==m1")
(intro 1)
(intro 0 (pt "n^1"))
(intro 0 (pt "m^1"))
(split)
(intro 0)
(use "n1==m1")
(split)
(use "n0=Sn1")
(use "m0=Sm1")
(assume "Assertion")
(assume "n^" "m^" "n==m")
(use "Assertion")
(intro 0 (pt "n^"))
(intro 0 (pt "m^"))
(split)
(intro 0)
(split)
(intro 0)
(use "n==m")
(save "CoEqPNatSuccRev")

;;Lemma1
(set-goal "all n^(CoTotal n^ -> all n (CoEqPNat n^ n -> F) -> CoEqPNat n^ inf)")
(assume "n^" "CoTn" "Hyp")
(assert "allnc m^(all n(CoEqPNat n^ n -> F) andi CoTotalNat n^ andi m^ eqd inf -> CoEqPNat n^ m^)")
(assume "m^")
(coind)
(assume "n^0" "m^0" "Conj")
(elim "Conj")
(assume "n0 not Total")
(elim)
(assume "CoTn0" "m0==inf")
(intro 1)
(inst-with-to "CoTotalNatClause" (pt "n^0") "CoTn0" "Inst")
(elim "Inst")
(assume "n0=0")
(use "Efq")
(use "n0 not Total" (pt "0"))
(simp "n0=0")
(use "CoEqPNatRefl")
(use "NatTotalToCoTotal")
(intro 0)
(assume "ExHyp")
(by-assume "ExHyp" "n^1" "n1Prop")
(intro 0 (pt "n^1"))
(intro 0 (pt "m^0"))
(split)
(intro 1)
(split)
(assume "n" "n1=n")
(use "n0 not Total" (pt "Succ n"))
(simp "n1Prop")
(use "CoEqPNatSuccRev")
(use "n1=n")
(split)
(use "n1Prop")
(use "m0==inf")
(split)
(use "n1Prop")
(use "EqDTrans" (pt "inf"))
(use "m0==inf")
(ng #t)
(simp (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))))
(ng #t)
(simp "m0==inf")
(ng #t)
(use "InitEqD")
(assume "AllHyp")
(use "AllHyp" (pt "inf"))
(split)
(use "Hyp")
(split)
(use "CoTn")
(use "InitEqD")
(save "Lemma1")

(set-goal "all boole (boole eqd True oru boole eqd False)")
(ind)
(intro 0)
(intro 0)
(intro 1)
(intro 0)
(save "BooleEqDDec")

;;Lemma2
(set-goal "allnc p^(allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) -> 
                  allnc n^,m^(CoEqPNat n^ m^ -> (p^ n^) eqd (p^ m^)) -> 
                  all n (p^ n) eqd False andi (p^ inf) eqd False -> all n^(CoTotal n^ -> (p^ n^) eqd False))")
(assume "p^" "pCoT" "pExt" "Hyp" "n^" "CoTn")
(assert "exl boole p^ n^ eqd boole")
(use "ExLTotalIntro")
(intro 0 (pt "p^ n^"))
(split)
(use "pCoT")
(use "CoTn")
(intro 0)
(assume "ExHyp")
(by-assume "ExHyp" "boole0" "pnDef")
(simp "pnDef")
(inst-with-to "BooleEqDDec" (pt "boole0") "Disj")
(elim "Disj")
(assume "pn=True")
(assert "all n(CoEqPNat n^ n -> F)")
(assume "n0" "n0==n")
(elim "Hyp")
(assume "AllHyp" "infHyp")
(inst-with-to "AllHyp" (pt "n0") "n0Prop")
(use "EqFalseToNeg" (pt "True"))
(simp "<-" "n0Prop")
(simp "<-" "pn=True")
(simp "<-" "pnDef")
(inst-with-to "pExt" (pt "n^") (pt "n0") "n0==n" "InstII")
(simp "InstII")
(simp "n0Prop")
(use "Truth")
(use "Truth")
(assume "AllHyp")
(assert "CoEqPNat n^ inf -> F")
(assume "n==inf")
(use "EqFalseToNeg" (pt "True"))
(inst-with-to "pExt" (pt "n^") (pt "inf") "n==inf" "InstII")
(elim "Hyp")
(assume "Useless" "pinfDef")
(simp "<-" "pinfDef")
(simp "<-" "pn=True")
(simp "<-" "pnDef")
(simp "InstII")
(simp "pinfDef")
(use "Truth")
(use "Truth")
(assume "n=/inf")
(simp "pn=True")
(use "BooleEqToEqD")
(use "AtomFalse")
(assume "Useless")
(use "n=/inf")
(use "Lemma1")
(use "CoTn")
(use "AllHyp")
(assume "HypIII")
(use "HypIII")
(save "Lemma2")

;;Prop 3
(set-goal "allnc p^(allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) -> 
                  CoTotalNat (eps p^))")
(assume "p^" "pCoExt")
;; (assert "exl boole boole eqd p^ 0")
;;  (use "ExLTotalIntro")
;;  (intro 0 (pt "p^ 0"))
;;  (split)
;;  (use "pCoExt")
;;  (use "NatTotalToCoTotal")
;;  (intro 0)
;;  (use "InitEqD")
;; (assume "ExHyp")
;;(by-assume "ExHyp" "boole" "p0Def")
(assert "exr p^0 (allnc n^(CoTotalNat n^ -> TotalBoole (p^0 n^)) andl eps p^ eqd (CoRec (nat=>boole)=>nat)p^0 phi)")
 (intro 0 (pt "p^"))
 (split)
 (use "pCoExt")
 (ng #t)
 (use "InitEqD")
(coind)
(assume "m^0" "Hyp")
(by-assume "Hyp" "p^0" "p0Prop")
(elim "p0Prop")
(assume "p0Ext" "m0Def")
(assert (make-all (pv "boole") (make-imp (pf "p^0 0 eqd boole") (proof-to-formula (current-goal)))))
(ind)
(assume "p0True")
(ng "m0Def")
(simphyp-to "m0Def" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "m0DefII")
(ng)
(simphyp-to "m0DefII" "p0True" "m0DefIII")
(ng)
(intro 0)
(use "m0DefIII")
(assume "p0False")
(ng "m0Def")
(simphyp-to "m0Def" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "m0DefII")
(ng)
(simphyp-to "m0DefII" "p0False" "m0DefIII")
(ng)
(intro 1)
(intro 0 (pt "((CoRec (nat=>boole)=>nat)([n]p^0(Succ n))
            ([p]
              [if (p 0)
                (DummyL nat ysum(nat=>boole))
                (Inr((InR nat=>boole nat)([n]p(Succ n))))]))"))
(ng)
(split)
(intro 1)
(intro 0 (pt "[n]p^0(Succ n)"))
(split)
(assume "n^" "CoTn")
(ng #t)
(use "p0Ext")
(use "NatSuccCoTotal")
(use "CoTn")
(use "InitEqD")
(use "m0DefIII")
(assume "AllHyp")
(assert "exl boole p^0 0 eqd boole")
 (use "ExLTotalIntro")
 (intro 0 (pt "p^0 0"))
 (split)
 (use "p0Prop")
 (use "NatTotalToCoTotal")
 (intro 0)
 (use "InitEqD")
(assume "ExHyp")
(by-assume "ExHyp" "boole" "p0Def")
(use "AllHyp" (pt "boole"))
(use "p0Def")
(save "epsExt")

(set-goal "allnc n^ (CoEqPNat (Succ n^) 0 -> F)")
(assume "n^" "Sn eqp 0")
(inst-with-to "CoEqPNatClause" (pt "Succ n^") (pt "0") "Sn eqp 0" "Inst")
(elim "Inst")
(elim)
(assume "Sn=0" "0=0")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "Succ n^ eqd 0")) (pt "n^") "Sn=0")
(use "Truth")
(use "Truth")
(assume "ExHyp")
(by-assume "ExHyp" "n^0" "n0Prop")
(by-assume "n0Prop" "n^1" "n0n1Prop")
(elim "n0n1Prop")
(assume "UselessI")
(elim)
(assume "UselessII" "0=Sn1")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "0 eqd Succ n^1")) (pt "n^1") "0=Sn1")
(use "Truth")
(use "Truth")
(save "CoEqPNatZeroSuccToFalsity")

(set-goal "allnc n^,m^(CoEqPNat n^ m^ -> CoEqPNat m^ n^)")
(assume "n^" "m^")
(coind)
(assume "n^0" "m^0" "m0=n0")
(inst-with-to "CoEqPNatClause" (pt "m^0") (pt "n^0") "m0=n0" "Inst")
(elim "Inst")
(assume "Conj")
(intro 0)
(split)
(use "Conj")
(use "Conj")
(assume "ExHyp")
(by-assume "ExHyp" "m^1" "m1Prop")
(by-assume "m1Prop" "n^1" "n1Prop")
(intro 1)
(intro 0 (pt "n^1"))
(intro 0 (pt "m^1"))
(split)
(intro 1)
(use "n1Prop")
(split)
(use "n1Prop")
(use "n1Prop")
(save "CoEqPNatSym")

(set-goal "all n^,m^(CoEqPNat (Succ n^) (Succ m^) -> CoEqPNat n^ m^)")
(assume "n^" "m^" "Sn=Sm")
(inst-with-to "CoEqPNatClause" (pt "Succ n^") (pt "Succ m^") "Sn=Sm" "Inst")
(elim "Inst")
(elim)
(assume "Sn=0" "Sm=0")
(use "Efq")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "Succ n^ eqd 0")) (pt "n^") "Sn=0")
(use "Truth")
(use "Truth")
(assume "ExHyp")
(by-assume "ExHyp" "n^0" "n0Prop")
(by-assume "n0Prop" "m^0" "n0m0Prop")
(simp (pf "n^ eqd n^0"))
(simp (pf "m^ eqd m^0"))
(use "n0m0Prop")
(use (constructor-eqd-imp-args-eqd-proof (pf "Succ m^ eqd Succ m^0")))
(use "n0m0Prop")
(use (constructor-eqd-imp-args-eqd-proof (pf "Succ n^ eqd Succ n^0")))
(use "n0m0Prop")
(save "CoEqPNatSucc")

;;Prop4
(set-goal "all n allnc p^(allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) -> 
                      CoEqPNat (eps p^) n -> (p^ n) eqd True)")
(ind)
(assume "p^" "pExt")
(ng #t)
(assert (make-all (pv "boole") (make-imp (pf "p^ 0 eqd boole") (proof-to-formula (current-goal)))))
(ind)
(assume "p0True" "Hyp")
(use "p0True")
(assume "p0False" "Hyp")
(simphyp-to "Hyp" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "HypII")
(ng)
(simphyp-to "HypII" "p0False" "HypIII")
(ng)
(use "Efq")
(use "CoEqPNatZeroSuccToFalsity" (pt "((CoRec (nat=>boole)=>nat)([n]p^(Succ n))
           ([p]
             [if (p 0)
               (DummyL nat ysum(nat=>boole))
               (Inr((InR nat=>boole nat)([n]p(Succ n))))]))"))
(use "HypIII")
(assume "AllHyp")
(assert "exl boole p^ 0 eqd boole")
 (use "ExLTotalIntro")
 (intro 0 (pt "p^ 0"))
 (split)
 (use "pExt")
 (use "NatTotalToCoTotal")
 (intro 0)
 (use "InitEqD")
(assume "ExHypII")
(by-assume "ExHypII" "boole" "p0Def")
(use "AllHyp" (pt "boole"))
(use "p0Def")
;;ind case
(assume "n" "IH" "p^" "pExt" "epspDef")
(simp (pf "p^(Succ n) eqd ([n](p^(Succ n)))n"))
(use "IH")
(ng #t)
(assume "n^" "CoTn")
(use "pExt")
(use "NatSuccCoTotal")
(use "CoTn")
(ng)
(assert (make-all (pv "boole") (make-imp (pf "p^ 0 eqd boole") (proof-to-formula (current-goal)))))
(ind)
(assume "p0True")
(simphyp-to "epspDef" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "HypII")
(ng)
(simphyp-to "HypII" "p0True" "HypIII")
(ng)
(use "Efq")
(use "CoEqPNatZeroSuccToFalsity" (pt "n"))
(use "CoEqPNatSym")
(use "HypIII")
(assume "p0False")
(simphyp-to "epspDef" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "HypII")
(ng)
(simphyp-to "HypII" "p0False" "HypIII")
(ng)
(use "CoEqPNatSucc")
(use "HypIII")
(assume "AllHyp")
(assert "exl boole p^ 0 eqd boole")
 (use "ExLTotalIntro")
 (intro 0 (pt "p^ 0"))
 (split)
 (use "pExt")
 (use "NatTotalToCoTotal")
 (intro 0)
 (use "InitEqD")
(assume "ExHyp")
(by-assume "ExHyp" "boole" "pDef")
(use "AllHyp" (pt "boole"))
(use "pDef")
(ng #t)
(use "InitEqD")
(save "Prop4")

;;Prop5
(set-goal "all n allnc p^(allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) -> 
                      CoEqPNat (eps p^) inf -> p^ n eqd False)")
(ind)
(assume "p^" "pExt" "eps p=inf")
(assert (make-all (pv "boole") (make-imp (pf "p^ 0 eqd boole") (proof-to-formula (current-goal)))))
(ind)
(assume "p0True")
(ng)
(simphyp-to "eps p=inf" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "HypII")
(ng)
(simphyp-to "HypII" "p0True" "HypIII")
(ng)
(simphyp-to "HypIII" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))) "HypIV")
(ng)
(use "Efq")
(use "CoEqPNatZeroSuccToFalsity" (pt "((CoRec unit=>nat)Dummy([unit]Inr((InR unit nat)unit)))"))
(use "CoEqPNatSym")
(use "HypIV")
(assume "p0False")
(use "p0False")
(assume "AllHyp")
(assert "exl boole p^ 0 eqd boole")
 (use "ExLTotalIntro")
 (intro 0 (pt "p^ 0"))
 (split)
 (use "pExt")
 (use "NatTotalToCoTotal")
 (intro 0)
 (use "InitEqD")
(assume "ExHyp")
(by-assume "ExHyp" "boole" "pDef")
(use "AllHyp" (pt "boole"))
(use "pDef")
(assume "n" "IH" "p^" "pExt" "eps p=inf")
(simp (pf "p^(Succ n) eqd ([n](p^(Succ n)))n"))
(use "IH")
(ng #t)
(assume "n^" "CoTn")
(use "pExt")
(use "NatSuccCoTotal")
(use "CoTn")
(ng)
(assert (make-all (pv "boole") (make-imp (pf "p^ 0 eqd boole") (proof-to-formula (current-goal)))))
(ind)
(assume "p0True")
(simphyp-to "eps p=inf" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "HypII")
(ng)
(simphyp-to "HypII" "p0True" "HypIII")
(ng)
(simphyp-to "HypIII" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))) "HypIV")
(ng)
(use "Efq")
(use "CoEqPNatZeroSuccToFalsity" (pt "((CoRec unit=>nat)Dummy([unit]Inr((InR unit nat)unit)))"))
(use "CoEqPNatSym")
(use "HypIV")
(assume "p0False")
(simphyp-to "eps p=inf" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "HypII")
(ng)
(simphyp-to "HypII" "p0False" "HypIII")
(ng)
(simphyp-to "HypIII" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))) "HypIV")
(ng)
(use "CoEqPNatSucc")
(use "HypIV")
(assume "AllHyp")
(assert "exl boole p^ 0 eqd boole")
 (use "ExLTotalIntro")
 (intro 0 (pt "p^ 0"))
 (split)
 (use "pExt")
 (use "NatTotalToCoTotal")
 (intro 0)
 (use "InitEqD")
(assume "ExHyp")
(by-assume "ExHyp" "boole" "pDef")
(use "AllHyp" (pt "boole"))
(use "pDef")
(ng #t)
(use "InitEqD")
(save "Prop5")

;;thm6
(set-goal "allnc p^(allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) -> 
                  allnc n^,m^(CoEqPNat n^ m^ -> (p^ n^) eqd (p^ m^)) -> 
                  p^(eps p^) eqd False -> allnc n^(CoTotal n^ -> (p^ n^) eqd False))")
(assume "p^" "pCoT" "pExt" "pDef" "n^" "CoTn")
(assert "all n (CoEqPNat (eps p^) n -> F)")
(assume "n" "eps p==n")
(inst-with-to "pExt" (pt "eps p^") (pt "n") "eps p==n" "Inst")
(simphyp-to "Inst" "pDef" "InstII")
(inst-with-to "Prop4" (pt "n") (pt "p^") "pCoT" "eps p==n" "Prop4Inst")
(use "EqFalseToNeg" (pt "True"))
(simp "InstII")
(simp "<-" "Prop4Inst")
(simp "Prop4Inst")
(use "Truth")
(use "Truth")
(assume "Claim0")
(assert "CoEqPNat (eps p^) inf")
(use "Lemma1")
(use "epsExt")
(use "pCoT")
(use "Claim0")
(assume "Claim1")
(assert "all n(p^ n eqd False)")
(assume "n")
(use "Prop5")
(use "pCoT")
(use "Claim1")
(assume "Claim2")
(assert "p^ inf eqd False")
(use "EqDTrans" (pt "p^ (eps p^)"))
(use "pExt")
(use "CoEqPNatSym")
(use "Claim1")
(use "pDef")
(assume "Claim3")
(use "Lemma2")
(use "pCoT")
(use "pExt")
(split)
(use "Claim2")
(use "Claim3")
(use "CoTn")
(save "Thm6")

;; N_inf searchable
(set-goal "allnc p^(allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) -> 
                  allnc n^,m^(CoEqPNat n^ m^ -> (p^ n^) eqd (p^ m^)) -> 
                  exr n^(CoTotalNat n^ andl p^ n^ eqd True) ori allnc n^(CoTotalNat n^ -> p^ n^ eqd False))")
(assume "p^" "pCoT" "pExt")
(assert (make-all (pv "boole") (make-imp (pf "p^(eps p^) eqd boole") (proof-to-formula (current-goal)))))
(ind)
(assume "pepspTrue")
(intro 0)
(intro 0 (pt "eps p^"))
(split)
(use "epsExt")
(use "pCoT")
(use "pepspTrue")
(assume "pepspFalse")
(intro 1)
(use "Thm6")
(use "pCoT")
(use "pExt")
(use "pepspFalse")
(assume "AllHyp")
(assert "exl boole p^ (eps p^) eqd boole")
(use "ExLTotalIntro")
(intro 0 (pt "p^ (eps p^)"))
(split)
(use "pCoT")
(use "epsExt")
(use "pCoT")
(intro 0)
(assume "ExHyp")
(by-assume "ExHyp" "boole" "bProp")
(use "AllHyp" (pt "boole"))
(use "bProp")
;;(cdp)
(save "NInfSearchable")

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

;; [p0]
;;  [if ((cExLTotalIntro boole)(p0(cepsExt p0))) (Inl(cepsExt p0)) (DummyR nat)]

(deanimate "epsExt")
(animate "ExLTotalIntro")
(pp (nt eterm))

;; [p0]
;; [if (p0
;;       ((CoRec (nat=>boole)=>nat)p0
;;        ([p1]
;;          [if (p1(cNatTotalToCoTotal 0))
;;            (DummyL nat ysum(nat=>boole))
;;            (Inr((InR nat=>boole nat)([n2]p1(cNatSuccCoTotal n2))))])))
;;   (Inl((CoRec (nat=>boole)=>nat)p0
;;       ([p1]
;;         [if (p1(cNatTotalToCoTotal 0))
;;           (DummyL nat ysum(nat=>boole))
;;           (Inr((InR nat=>boole nat)([n2]p1(cNatSuccCoTotal n2))))])))
;;   (DummyR nat)]

(add-ids
 (list (list "LtNat" (make-arity (py "nat") (py "nat")) "nat"))
 '("allnc n^ LtNat Zero (Succ n^)" "Init")
 '("allnc n^,m^(LtNat n^ m^ -> LtNat (Succ n^) (Succ m^))"))

(add-token
 "<<"
 'pred-infix
 (lambda(x y)
   (make-predicate-formula (make-idpredconst "LtNat" '() '()) x y)))

(add-idpredconst-display "LtNat" 'pred-infix "<<")

(set-goal "allnc n^,m^(n^ << m^ -> Total n^)")
(assume "n^" "l^")
(elim)
(assume "m^")
(intro 0)
(assume "m^0" "m^1" "n<m" "Tm0")
(intro 1)
(use "Tm0")
(save "LtNatToTotal")

(set-goal "all n(n<<0 -> F)")
(ind)
(assume "0<0")
(assert "all m0,m1(m0<<m1 -> m0 eqd 0 -> m1 eqd 0 -> F)")
(assume "m0" "m1")
(elim)
(assume "n^" "0=0" "Sn=0")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "Succ n^ eqd 0")) (pt "n^") "Sn=0")
(use "Truth")
(use "Truth")
(assume "n^" "m^" "n<m" "IH" "Sn=0" "Sm=0")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "Succ n^ eqd 0")) (pt "n^") "Sn=0")
(use "Truth")
(use "Truth")
(assume "Hyp")
(use "Hyp" (pt "0") (pt "0"))
(use "0<0")
(intro 0)
(intro 0)
(assume "n" "IH" "Sn<0")
(assert "all m0,m1(m0<<m1 -> m0 eqd Succ n -> m1 eqd 0 -> F)")
(assume "m0" "m1")
(elim)
(assume "n^0" "0=Sn0" "Sn0=0")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "Succ n^ eqd 0")) (pt "n^0") "Sn0=0")
(use "Truth")
(use "Truth")
(assume "n^0" "m^0" "n0<m0" "IH2" "Sn0=Sm0" "Sm0=0")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "Succ n^ eqd 0")) (pt "m^0") "Sm0=0")
(use "Truth")
(use "Truth")
(assume "Hyp")
(use "Hyp" (pt "Succ n") (pt "0"))
(use "Sn<0")
(intro 0)
(intro 0)
(save "LtNatZeroToFalsity")

(set-goal "allnc n^,m^(n^ <<m^ -> 0<<n^ -> Pred n^ << Pred m^)")
(assume "n^" "m^")
(elim)
(assume "n^0")
(assume "0<0")
(use "Efq")
(use "LtNatZeroToFalsity" (pt "0"))
(use "0<0")
(assume "n^0" "m^0" "n0<m0" "IH" "0<Sn0")
(ng #t)
(use "n0<m0")
(save "LtNatPred")

(set-goal "allnc n^,m^(Succ n^ <<Succ m^ -> n^ <<m^)")
(assert "allnc n^0,n^1,m^0,m^1(n^1<<m^1 -> n^1 eqd Succ n^0 -> m^1 eqd Succ m^0 -> n^0 << m^0)")
(assume "n^0" "n^1" "m^0" "m^1")
(elim)
(assume "n^" "0=Sn0")
(use "Efq")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "0 eqd Succ n^0")) (pt "n^0") "0=Sn0")
(use "Truth")
(use "Truth")
(assume "n^2" "m^2" "n2<m2" "IH" "Sn2=Sn0" "Sm2=Sm0")
(assert "n^2 eqd n^0")
(use (constructor-eqd-imp-args-eqd-proof (pf "Succ n^2 eqd Succ n^0")))
(use "Sn2=Sn0")
(assume "n2=n0")
(simp "<-" "n2=n0")
(assert "m^2 eqd m^0")
(use (constructor-eqd-imp-args-eqd-proof (pf "Succ m^2 eqd Succ m^0")))
(use "Sm2=Sm0")
(assume "m2=m0")
(simp "<-" "m2=m0")
(use "n2<m2")
(assume "AllHyp" "n^" "m^" "Sn<Sm")
(use "AllHyp" (pt "Succ n^") (pt "Succ m^"))
(use "Sn<Sm")
(intro 0)
(intro 0)
(save "NatSuccLt")

(set-goal "allnc n^,m^(n^ <<m^ -> Succ(Pred m^) eqd m^)")
(assume "n^" "m^")
(elim)
(assume "m^0")
(ng #t)
(intro 0)
(assume "n^0" "m^0" "n0<m0" "PSm=m")
(ng #t)
(intro 0)
(save "LtNatToSuccPredEqD")

(set-goal "allnc n^,m^,l^(n^ <<m^ -> m^ <<l^ -> n^ <<l^)")
(assert  "allnc n^,m^(n^ <<m^ -> allnc l^( m^ <<l^ -> n^ <<l^))")
(assume "n^" "m^")
(elim)
(assume "n^0" "l^0")
(elim)
(assume "l^1")
(intro 0)
(assume "m^1" "l^1" "m1<l1" "0<l1")
(intro 0)
(assume "n^0" "m^0" "n0<m0" "IH" "l^" "Sm0<l")
(assert "Pred (Succ m^0) << Pred l^")
(use "LtNatPred")
(use "Sm0<l")
(intro 0)
(assume "m0<Pred l")
(ng "m0<Pred l")
(assert "n^0<<Pred l^")
(use "IH")
(use "m0<Pred l")
(assume "n0<Pred l")
(inst-with-to "LtNatToSuccPredEqD" (pt "Succ m^0") (pt "l^") "Sm0<l" "Inst")
(simp "<-" "Inst")
(intro 1)
(use "n0<Pred l")
(assume "AllHyp" "n^" "m^" "l^" "n<m" "m<l")
(use "AllHyp" (pt "m^"))
(auto)
(save "LtNatTrans")

(set-goal "TotalNat inf -> F")
(assert "allnc n^ (TotalNat n^ -> CoEqP n^ inf -> F)")
(assume "l^0")
(elim)
(assume "0===inf")
(inst-with-to "CoEqPNatClause" (pt "Zero") (pt "inf") "0===inf" "Inst")
(elim "Inst")
(elim)
(assume "0=0" "0=inf")
(ng "0===inf")
(simphyp-to "0===inf" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))) "0===S inf")
(ng "0===S inf")
(use "CoEqPNatZeroSuccToFalsity" (pt "inf"))
(ng #t)
(use "CoEqPNatSym")
(use "0===S inf")
(assume "ExHyp")
(by-assume "ExHyp" "n^0" "n0Prop")
(by-assume "n0Prop" "n^1" "n0n1Prop")
(elim "n0n1Prop")
(assume "n0===n1")
(elim)
(assume "0=Sn0" "inf===Sn1")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "0 eqd Succ n^0")) (pt "n^0") "0=Sn0")
(use "Truth")
(use "Truth")
(assume "n^" "Tn" "IH" "Sn===inf")
(ng "Sn===inf")
(simphyp-to "Sn===inf" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))) "Sn===S inf")
(ng "Sn===S inf")
(use "IH")
(use "CoEqPNatSucc")
(ng #t)
(use "Sn===S inf")
(assume "AllHyp" "Tinf")
(use "AllHyp" (pt "inf"))
(use "Tinf")
(use "CoEqPNatRefl")
(use "infCoTotal")
(save "TotalInfToFalsity")

(set-goal "all n(inf <<n -> F)")
(assume "n" "inf<n")
(use "TotalInfToFalsity")
(use "LtNatToTotal" (pt "n"))
(use "inf<n")
(save "LtNatInfToFalsity")

(set-goal "inf<<inf -> F")
(use "LtNatInfToFalsity")

(set-goal "allnc n^(n^ <<n^ -> F)")
(assert "allnc n^,m^(n^ <<m^ -> n^ eqd m^ -> F)")
(assume "n^0" "n^1")
(elim)
(assume "n^" "0=Sn")
(use "EqFalseToNeg" (pt "True"))
(simp-with (constructors-overlap-imp-falsity-proof (pf "0 eqd Succ n^")) (pt "n^") "0=Sn")
(use "Truth")
(use "Truth")
(assume "n^" "m^" "n<m" "IH" "Sn=Sm")
(use "IH")
(use (constructor-eqd-imp-args-eqd-proof (pf "Succ n^ eqd Succ m^")))
(use "Sn=Sm")
(assume "AllHyp")
(assume "n^" "n<n")
(use "AllHyp" (pt "n^") (pt "n^"))
(use "n<n")
(intro 0)
(save "LtNatReflToFalsity")

(add-algs "AppartAlg" '("Left" "nat=>AppartAlg") '("Right" "nat=>AppartAlg"))

(add-ids
 (list (list "Appart" (make-arity (py "nat") (py "nat")) "AppartAlg"))
 '("allnc n^,m^(n^ << m^ -> Appart n^ m^)" "AppartLeftIntro")
 '("allnc n^,m^(m^ << n^ -> Appart n^ m^)" "AppartRightIntro"))

(add-token
 "#"
 'pred-infix
 (lambda(x y)
   (make-predicate-formula (make-idpredconst "Appart" '() '()) x y)))

(add-idpredconst-display "Appart" 'pred-infix "#")

;;# appartness relation
(set-goal "allnc n^(n^ # n^ -> F)")
(assert "allnc n^,m^(n^ # m^ -> n^ eqd m^ -> F)")
(assume "n^" "m^")
(elim)
(assume "n^0" "m^0" "n0<m0" "n0=m0")
(use "LtNatReflToFalsity" (pt "n^0"))
(assert "allnc l^(n^0 eqd l^ -> n^0<<n^0)")
(assume "l^" "n0=l")
(use "LtNatTrans" (pt "m^0"))
(use "n0<m0")
(simp "n0=l")
(simp "<-" "n0=m0")
(simp (pf "l^ eqd m^0"))
(use "n0<m0")
(simp "<-" "n0=l")
(use "n0=m0")
(assume "AllHyp")
(use "AllHyp" (pt "n^0"))
(intro 0)
(assume "n^0" "m^0" "m0<n0" "n0=m0")
(use "LtNatReflToFalsity" (pt "m^0"))
(assert "allnc l^(m^0 eqd l^ -> m^0<<m^0)")
(assume "l^" "m0=l")
(use "LtNatTrans" (pt "n^0"))
(use "m0<n0")
(simp "m0=l")
(simp "n0=m0")
(simp (pf "l^ eqd n^0"))
(use "m0<n0")
(simp "<-" "m0=l")
(simp "n0=m0")
(intro 0)
(assume "AllHyp")
(use "AllHyp" (pt "m^0"))
(intro 0)
(assume "AllProp" "n^" "n#n")
(use "AllProp" (pt "n^") (pt "n^"))
(use "n#n")
(intro 0)
(save "AppartIrRefl")

(set-goal "allnc n^,m^(n^ # m^ -> m^ # n^)")
(assume "n^" "m^")
(elim)
(assume "n^0" "m^0" "n0<m0")
(intro 1)
(use "n0<m0")
(assume "n^0" "m^0" "m0<n0")
(intro 0)
(use "m0<n0")
(save "AppartSym")

(set-goal "allnc n^(CoTotal n^ -> CoTotal (Pred n^))")
(assert "allnc n^(exr m^(CoTotal m^ andi n^ eqd Pred m^) -> CoTotalNat n^)")
(assume "n^")
(coind)
(assume "n^0" "ExHyp")
(by-assume "ExHyp" "m^0" "m0Prop")
(elim "m0Prop")
(assume "CoTm0" "n0=Pm0")
(inst-with-to "CoTotalNatClause" (pt "m^0") "CoTm0" "Inst")
(elim "Inst")
(assume "m0=0")
(intro 0)
(simp "n0=Pm0")
(simp "m0=0")
(ng #t)
(intro 0)
(assume "ExHypII")
(by-assume "ExHypII" "m^1" "m1Prop")
(elim "m1Prop")
(assume "CoTm1" "m0=Sm1")
(inst-with-to "CoTotalNatClause" (pt "m^1") "CoTm1" "InstII")
(elim "InstII")
(assume "m1=0")
(intro 0)
(simp "n0=Pm0")
(simp "m0=Sm1")
(simp "m1=0")
(ng #t)
(intro 0)
(assume "ExHypIII")
(by-assume "ExHypIII" "m^2" "m2Prop")
(intro 1)
(intro 0 (pt "m^2"))
(split)
(intro 0)
(use "m2Prop")
(simp "n0=Pm0")
(simp "m0=Sm1")
(simp "m2Prop")
(ng #t)
(intro 0)
(assume "AllProp" "n^" "CoTn")
(use "AllProp")
(intro 0 (pt "n^"))
(split)
(use "CoTn")
(intro 0)
(save "NatPredCoTotal")

(set-goal "all n allnc m^(CoTotalNat m^ -> n <<m^ -> allnc l^(CoTotalNat l^ -> n <<l^ ori l^ <<m^))")
(ind)
(assume "m^" "CoTm" "0<m" "l^" "CoTl")
(inst-with-to "CoTotalNatClause" (pt "l^") "CoTl" "CoTotalNatClauseInst")
(elim "CoTotalNatClauseInst")
(assume "l=0")
(intro 1)
(simp "l=0")
(use "0<m")
(assume "ExHyp")
(by-assume "ExHyp" "l^0" "l0Prop")
(intro 0)
(simp "l0Prop")
(intro 0)
(assume "n" "IH" "m^" "CoTm" "Sn<m" "l^" "CoTl")
(inst-with-to "CoTotalNatClause" (pt "l^") "CoTl" "CoTotalNatClauseInst")
(elim "CoTotalNatClauseInst")
(assume "l=0")
(intro 1)
(simp "l=0")
(use "LtNatTrans" (pt "Succ n"))
(intro 0)
(use "Sn<m")
(assume "ExHyp")
(by-assume "ExHyp" "l^1" "l1Prop")
(elim "l1Prop")
(assume "CoTl1" "l=Sl1")
(cut "CoTotalNat (Pred m^)")
(assume "CoTPm")
(cut "n<<Pred m^")
(assume "n<Pm")
(inst-with-to "IH" (pt "Pred m^") "CoTPm" "n<Pm" (pt "l^1") "CoTl1" "Inst")
(elim "Inst")
(assume "n<l1")
(intro 0)
(simp "l=Sl1")
(intro 1)
(use "n<l1")
(assume "l1<Pm")
(intro 1)
(simp "l=Sl1")
(simp (pf "m^ eqd Succ(Pred m^)"))
(intro 1)
(use "l1<Pm")
(simp "LtNatToSuccPredEqD" (pt "Succ n"))
(intro 0)
(use "Sn<m")
(use "NatSuccLt")
(simp "LtNatToSuccPredEqD" (pt "Succ n"))
(use "Sn<m")
(use "Sn<m")
(use "NatPredCoTotal")
(use "CoTm")
(save "NatLtApproxSplit")

;;CoTransitivity
(set-goal "allnc n^,m^,l^(n^ #m^ -> CoTotalNat m^ -> CoTotalNat n^ -> CoTotalNat l^ -> n^ #l^ ori l^ #m^)")
(assume "n^" "m^" "l^")
(elim)
(assume "n^0" "m^0" "n0<m0" "CoTm0" "CoTn0" "CoTl")
(assert "allnc n^1(Total n^1 -> n^1 eqd n^0 -> n^0#l^ ori l^ #m^0)")
(use "AllTotalElim")
(assume "n" "n=n0")
(simp "<-" "n=n0")
(assert "n<<m^0")
(simp "n=n0")
(use "n0<m0")
(assume "n<m0")
(inst-with-to "NatLtApproxSplit" (pt "n") (pt "m^0") "CoTm0" "n<m0" (pt "l^") "CoTl" "Inst")
(elim "Inst")
(assume "n<l")
(intro 0)
(intro 0)
(use "n<l")
(assume "l<m0")
(intro 1)
(intro 0)
(use "l<m0")
(assume "AllProp")
(use "AllProp" (pt "n^0"))
(use "LtNatToTotal" (pt "m^0"))
(use "n0<m0")
(intro 0)
(assume "n^0" "m^0" "m0<n0" "CoTm0" "CoTn0" "CoTl")
(assert "allnc n^1(Total n^1 -> n^1 eqd m^0 -> n^0#l^ ord l^ #m^0)")
(use "AllTotalElim")
(assume "n" "n=m0")
(simp "<-" "n=m0")
(assert "n<<n^0")
(simp "n=m0")
(use "m0<n0")
(assume "n<n0")
(inst-with-to "NatLtApproxSplit" (pt "n") (pt "n^0") "CoTn0" "n<n0" (pt "l^") "CoTl" "Inst")
(elim "Inst")
(assume "n<l")
(intro 1)
(intro 1)
(use "n<l")
(assume "l<n0")
(intro 0)
(intro 1)
(use "l<n0")
(assume "AllProp")
(use "AllProp" (pt "m^0"))
(use "LtNatToTotal" (pt "n^0"))
(use "m0<n0")
(intro 0)
(save "AppartCoTransitive")
;; (cdp)

(set-goal "allnc n^(CoTotal n^ -> n^ # inf -> Total n^)")
(assert "allnc n^,m^(CoTotal n^ -> n^ # m^ -> m^ eqd inf -> Total n^)")
(assume "n^" "m^" "CoTn")
(elim)
(assume "n^0" "m^0" "n0<m0" "m0=inf")
(use "LtNatToTotal" (pt "m^0"))
(use "n0<m0")
(assume "n^0" "m^0" "m0<n0" "m0=inf")
(use "Efq")
(use "TotalInfToFalsity")
(use "LtNatToTotal" (pt "n^0"))
(simp "<-" "m0=inf")
(use "m0<n0")
(assume "AllProp" "n^" "CoTn" "n app inf")
(use "AllProp" (pt "inf"))
(use "CoTn")
(use "n app inf")
(intro 0)
(save "NatAppartInfToTotal") 

;;tightness (prop eqd?)
(set-goal "allnc n^,m^((n^ #m^ -> F) -> CoEqPNat n^ m^)")

(set-goal "allnc p^(all n Total (p^ n) andi Total (p^ inf) -> allnc n^(CoTotal n^ -> Total (p^ n^)))")
(assume "p^" "Conj" "n^" "CoTn")

(set-goal "all n allnc m^(CoTotal m^ -> m^ min n << (Succ n))")
(ind)
(assume "m^" "CoTm")
(ng #t)
(intro 0)
(assume "n" "IH" "m^" "CoTm")
(ng #t)
(inst-with-to "CoTotalNatClause" (pt "m^") "CoTm" "Inst")
(elim "Inst")
(assume "m=0")
(simp "m=0")
(ng #t)
(intro 0)
(assume "ExHyp")
(by-assume "ExHyp" "m^1" "m1Prop")
(simp "m1Prop")
(ng #t)
(intro 1)
(use "IH")
(use "m1Prop")
(save "NatLtMin")

(set-goal "all n0 allnc m^(CoTotal m^ -> m^ min n0<<m^ -> m^ min n0 eqd n0)")
(ind)
(assume "m^" "CoTm" "min m 0<m")
(ng #t)
(intro 0)
(assume "n" "IH" "m^" "CoTm" "min m Sn <m")
(ng #t)
(inst-with-to "CoTotalNatClause" (pt "m^") "CoTm" "mProp")
(elim "mProp")
(assume "m=0")
(simphyp-to "min m Sn <m" "m=0" "Prop")
(use "Efq")
(use "LtNatZeroToFalsity" (pt "0"))
(use "Prop")
(assume "ExHyp")
(by-assume "ExHyp" "m^0" "m0Prop")
(simp "m0Prop")
(ng #t)
(simp (pf "m^0 min n eqd n"))
(intro 0)
(use "IH")
(use "m0Prop")
(use "NatSuccLt")
(simp "<-" "NatMin2CompRule")
(simp "<-" "m0Prop")
(use "min m Sn <m")
(save "NatLtMinTwo")

(set-goal "allnc m^(CoTotal m^ -> 0 min m^ eqd 0)")
(assume "m^" "CoTm")
(inst-with-to "CoTotalNatClause" (pt "m^") "CoTm" "Inst")
(elim "Inst")
(assume "m=0")
(simp "m=0")
(ng #t)
(intro 0)
(assume "ExHyp")
(by-assume "ExHyp" "m^0" "m0Prop")
(simp "m0Prop")
(ng #t)
(intro 0)
(save "NatMinZero")

(set-goal "all n allnc m^(CoTotal m^ -> m^ min n << m^ -> n<<m^)")
(ind)
(assume "m^" "CoTm" "0<m")
(simp (pf "0 eqd m^ min 0"))
(use "0<m")
(ng #t)
(intro 0)
(assume "n" "IH" "m^" "CoTm" "Hyp")
(inst-with-to "CoTotalNatClause" (pt "m^") "CoTm" "Inst")
(elim "Inst")
(assume "m=0")
(simphyp-to "Hyp" "m=0" "Prop")
(ng "Prop")
(use "Efq")
(use "LtNatZeroToFalsity" (pt "0"))
(use "Prop")
(assume "ExHyp")
(by-assume "ExHyp" "m^0" "m0Prop")
(simp "m0Prop")
(intro 1)
(use "IH")
(use "m0Prop")
(simphyp-to "Hyp" "m0Prop" "HypII")
(ng "HypII")
(use "NatSuccLt")
(use "HypII")
(save "NatLtMinThree")

(set-goal "allnc n^,m^(CoTotal n^ -> CoTotal m^ -> m^ << (Succ n^) -> m^ min n^ eqd m^)")
(assert "allnc m^(Total m^ ->  allnc n^(CoTotal n^ -> m^ <<(Succ n^) -> m^ min n^ eqd m^))")
(assume "m^")
(elim)
(assume "n^" "CoTn" "0<Sn")
(simp "NatMinZero")
(intro 0)
(use "CoTn")
(assume "n^" "Tn" "IH" "n^0" "CoTn0" "Sn<Sn0")
(inst-with-to "CoTotalNatClause" (pt "n^0") "CoTn0" "Inst")
(elim "Inst")
(assume "n0=0")
(simphyp-to "Sn<Sn0" "n0=0" "HypI")
(use "Efq")
(assert "exl m(Succ m eqd Succ n^)")
(use "ExLTotalIntro")
(intro 0 (pt "n^"))
(split)
(use "LtNatToTotal" (pt "0"))
(use "NatSuccLt")
(use "HypI")
(intro 0)
(assume "ExHypII")
(by-assume "ExHypII" "m" "nTotalDef")
(use "LtNatZeroToFalsity" (pt "m"))
(simp (pf "m eqd n^"))
(use "NatSuccLt")
(use "HypI")
(use (constructor-eqd-imp-args-eqd-proof (pf "Succ m eqd Succ n^")))
(use "nTotalDef")
(assume "ExHyp")
(by-assume "ExHyp" "m^0" "m0Prop")
(simp "m0Prop")
(ng #t)
(simp (pf "n^ min m^0 eqd n^"))
(intro 0)
(use "IH")
(use "m0Prop")
(use "NatSuccLt")
(simp "<-" "m0Prop")
(use "Sn<Sn0")
(assume "AllProp" "n^" "m^" "CoTn" "CoTm" "m<Sn")
(use "AllProp")
(use "LtNatToTotal" (pt "Succ n^"))
(use "m<Sn")
(use "CoTn")
(use "m<Sn")
(save "LtNatMinFour")

(set-goal "all n allnc m^(CoTotal m^ -> Total (m^ min n))")
(ind)
(assume "m^" "CoTm")
(ng #t)
(intro 0)
(assume "n" "IH" "m^" "CoTm")
(inst-with-to "CoTotalNatClause" (pt "m^") "CoTm" "Inst")
(elim "Inst")
(assume "m=0")
(simp "m=0")
(ng #t)
(intro 0)
(assume "ExHyp")
(by-assume "ExHyp" "m^0" "m0Prop")
(simp "m0Prop")
(ng #t)
(intro 1)
(use "IH")
(use "m0Prop")
(save "NatMinRhtTotalToTotal")

;;extension of eventually constant
(set-goal "allnc p^(all n(TotalBoole (p^ n)) -> exl n0 allnc m^(n0<<m^ -> (p^ n0) eqd (p^ m^)) -> allnc m^(CoTotal m^ -> TotalBoole (p^ m^)))")
(assume "p^" "pExt" "ExHyp")
(by-assume "ExHyp" "n0" "n0Prop")
(assert "allnc m^(CoTotal m^ -> (p^ (m^ min n0)) eqd p^ m^)")
(assume "m^" "CoTm")
(cut "m^ min n0<< m^ ord m^ << Succ n0")
(elim)
;; Case 1
(assume "min m n0<m")
(simp-with "NatLtMinTwo" (pt "n0") (pt "m^") "CoTm" "min m n0<m")
(use "n0Prop")
(use "NatLtMinThree")
(use "CoTm")
(use "min m n0<m")
;; Case 2
(assume "m<Sn0")
(simp "LtNatMinFour")
(intro 0)
(use "m<Sn0")
(use "CoTm")
(use "NatTotalToCoTotal")
(use "NatTotalVar")
(assert "exl m0 m0 eqd m^ min n0")
(use "ExLTotalIntro")
(intro 0 (pt "m^ min n0"))
(split)
(use "NatMinRhtTotalToTotal")
(use "CoTm")
(intro 0)
(assume "ExHypIII")
(by-assume "ExHypIII" "m0" "m0Prop")
(simp "<-" "m0Prop")
(use "NatLtApproxSplit")
(use "NatTotalToCoTotal")
(intro 1)
(use "NatTotalVar")
(simp "m0Prop")
(use "NatLtMin")
(use "CoTm")
(use "CoTm")
(assume "AllHyp" "m^" "CoTm")
(simp "<-" "AllHyp")
(assert "exl m0 m0 eqd m^ min n0")
(use "ExLTotalIntro")
(intro 0 (pt "m^ min n0"))
(split)
(use "NatMinRhtTotalToTotal")
(use "CoTm")
(intro 0)
(assume "ExHypIII")
(by-assume "ExHypIII" "m0" "m0Prop")
(simp "<-" "m0Prop")
(use "pExt")
(use "CoTm")
(save "EventuallyConstantExtension")

;; (animate "NatMinRhtTotalToTotal")
;; (pp (nt (proof-to-extracted-term)))

(set-goal "allnc p^(allnc n^(TotalNat n^ -> TotalBoole (p^ n^)) -> 
                  CoTotalNat (eps p^))")
(assume "p^" "pCoExt")
;; (assert "exl boole boole eqd p^ 0")
;;  (use "ExLTotalIntro")
;;  (intro 0 (pt "p^ 0"))
;;  (split)
;;  (use "pCoExt")
;;  (use "NatTotalToCoTotal")
;;  (intro 0)
;;  (use "InitEqD")
;; (assume "ExHyp")
;;(by-assume "ExHyp" "boole" "p0Def")
(assert "exr p^0 (allnc n^(TotalNat n^ -> TotalBoole (p^0 n^)) andl eps p^ eqd (CoRec (nat=>boole)=>nat)p^0 phi)")
 (intro 0 (pt "p^"))
 (split)
 (use "pCoExt")
 (ng #t)
 (use "InitEqD")
(coind)
(assume "m^0" "Hyp")
(by-assume "Hyp" "p^0" "p0Prop")
(elim "p0Prop")
(assume "p0Ext" "m0Def")
(assert (make-all (pv "boole") (make-imp (pf "p^0 0 eqd boole") (proof-to-formula (current-goal)))))
(ind)
(assume "p0True")
(ng "m0Def")
(simphyp-to "m0Def" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "m0DefII")
(ng)
(simphyp-to "m0DefII" "p0True" "m0DefIII")
(ng)
(intro 0)
(use "m0DefIII")
(assume "p0False")
(ng "m0Def")
(simphyp-to "m0Def" (make-proof-in-aconst-form (alg-or-arrow-types-to-corec-aconst (py "(nat=>boole)=>nat"))) "m0DefII")
(ng)
(simphyp-to "m0DefII" "p0False" "m0DefIII")
(ng)
(intro 1)
(intro 0 (pt "((CoRec (nat=>boole)=>nat)([n]p^0(Succ n))
            ([p]
              [if (p 0)
                (DummyL nat ysum(nat=>boole))
                (Inr((InR nat=>boole nat)([n]p(Succ n))))]))"))
(ng)
(split)
(intro 1)
(intro 0 (pt "[n]p^0(Succ n)"))
(split)
(assume "n^" "CoTn")
(ng #t)
(use "p0Ext")
(intro 1)
(use "CoTn")
(use "InitEqD")
(use "m0DefIII")
(assume "AllHyp")
(assert "exl boole p^0 0 eqd boole")
 (use "ExLTotalIntro")
 (intro 0 (pt "p^0 0"))
 (split)
 (use "p0Prop")
 (intro 0)
 (use "InitEqD")
(assume "ExHyp")
(by-assume "ExHyp" "boole" "p0Def")
(use "AllHyp" (pt "boole"))
(use "p0Def")
(save "epsExtTotal")

;; the assumptions about p are equivalent to ext

(set-goal "allnc p^(allnc n^,m^(CoEqPNat n^ m^ -> EqPBoole (p^ n^) (p^ m^)) -> allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) andi allnc n^,m^(CoEqPNat n^ m^ -> p^ n^ eqd p^ m^))")
(assume "p^" "pExt")
(split)
(assume "n^" "CoTn")
(use "EqPBooleToTotalLeft" (pt "p^ n^"))
(use "pExt")
(use "CoEqPNatRefl")
(use "CoTn")
(assume "n^" "m^" "n=m")
(use "EqPBooleToEqD")
(use "pExt")
(use "n=m")

(set-goal "allnc n^,m^(CoEqPNat n^ m^ -> CoTotalNat n^)")
(assert "allnc n^(exr m^ CoEqPNat n^ m^ -> CoTotalNat n^)")
(assume "n^")
(coind)
(assume "n^0" "ExHyp")
(by-assume "ExHyp" "m^0" "m0Prop")
(inst-with-to "CoEqPNatClause" (pt "n^0") (pt "m^0") "m0Prop" "Inst")
(elim "Inst")
(assume "n0=m0=0")
(intro 0)
(simp "n0=m0=0")
(intro 0)
(assume "ExHypII")
(by-assume "ExHypII" "n^1" "n1Prop")
(by-assume "n1Prop" "m^1" "n1m1Prop")
(intro 1)
(intro 0 (pt "n^1"))
(split)
(intro 1)
(intro 0 (pt "m^1"))
(use "n1m1Prop")
(use "n1m1Prop")
(assume "AllHyp")
(assume "n^" "m^" "n=m")
(use "AllHyp")
(intro 0 (pt "m^"))
(use "n=m")
(save "CoEqPNatToCoTotalLeft")

(set-goal "allnc p^(allnc n^(CoTotalNat n^ -> TotalBoole (p^ n^)) -> allnc n^,m^(CoEqPNat n^ m^ -> p^ n^ eqd p^ m^) -> allnc n^,m^(CoEqPNat n^ m^ -> EqPBoole (p^ n^) (p^ m^)))")
(assume "p^" "pCoTotalToTotal" "pWeakExt" "n^" "m^" "n=m")
(inst-with-to "pWeakExt" (pt "n^") (pt "m^") "n=m" "Inst")
(simp "Inst")
(use "EqPBooleRefl")
(use "pCoTotalToTotal")
(use "CoEqPNatToCoTotalLeft" (pt "n^"))
(use "CoEqPNatSym")
(use "n=m")