;; 2024-04-09.  nat.scm

;; (load "~/git/minlog/init.scm")
 
(display "loading nat.scm ...") (newline)

(add-algs "nat" '("Zero" "nat") '("Succ" "nat=>nat"))
(add-var-name "n" "m" "l" (py "nat")) ;l instead of k, which will be an int

(define (make-numeric-term-wrt-nat n)
  (if (= n 0)
      (pt "Zero")
      (make-term-in-app-form
       (pt "Succ")
       (make-numeric-term-wrt-nat (- n 1)))))

;; The following is in term.scm, because it is used for term-to-expr
;; (define (is-numeric-term-wrt-nat? term)
;;   (or
;;    (and (term-in-const-form? term)
;; 	(string=? "Zero" (const-to-name (term-in-const-form-to-const term))))
;;    (and (term-in-app-form? term)
;; 	(let ((op (term-in-app-form-to-op term)))
;; 	  (and (term-in-const-form? op)
;; 	       (string=? "Succ" (const-to-name
;; 				 (term-in-const-form-to-const op)))
;; 	       (is-numeric-term-wrt-nat? (term-in-app-form-to-arg term)))))))

;; (define (numeric-term-wrt-nat-to-number term)
;;   (if (equal? term (pt "Zero"))
;;       0
;;       (+ 1 (numeric-term-wrt-nat-to-number (term-in-app-form-to-arg term)))))

;; The functions make-numeric-term (used by the parser) and
;; is-numeric-term?, numeric-term-to-number (used by term-to-expr and
;; token-tree-to-string) take either pos or nat as default.

(define NAT-NUMBERS #t)

(define (make-numeric-term x)
  (if NAT-NUMBERS
      (make-numeric-term-wrt-nat x)
      (make-numeric-term-wrt-pos x)))

(define (is-numeric-term? x)
  (if NAT-NUMBERS
      (is-numeric-term-wrt-nat? x)
      (is-numeric-term-wrt-pos? x)))

(define (numeric-term-to-number x)
  (if NAT-NUMBERS
      (numeric-term-wrt-nat-to-number x)
      (numeric-term-wrt-pos-to-number x)))

(add-totality "nat")

;; This adds the c.r. predicate TotalNat with clauses
;; TotalNatZero:	TotalNat Zero
;; TotalNatSucc:	allnc nat^(TotalNat nat^ -> TotalNat(Succ nat^))

(add-totalnc "nat")
(add-co "TotalNat")
(add-co "TotalNatNc")

(add-mr-ids "TotalNat")
(add-co "TotalNatMR")

(add-eqp "nat")
(add-eqpnc "nat")
(add-co "EqPNat")
(add-co "EqPNatNc")

(add-mr-ids "EqPNat")
(add-co "EqPNatMR")

;; Code discarded 2019-05-14
;; (add-ext "nat")
;; (add-extnc "nat")

;; NatTotalVar
(set-goal "all n TotalNat n")
(use "AllTotalIntro")
(assume "n^" "Tn")
(use "Tn")
;; Proof finished
;; (cp)
(save "NatTotalVar")

;; We collect properties of TotalNat and EqPNat, including the Nc, Co
;; and MR variants.  These are

;; EfTotalNat
;; EfTotalNatNc
;; TotalNatToCoTotal
;; TotalNatNcToCoTotalNc
;; EfCoTotalNat
;; EfCoTotalNatNc
;; EfCoTotalNatMR
;; TotalNatMRToEqD
;; TotalNatMRToTotalNcLeft
;; TotalNatMRToTotalNcRight
;; TotalNatMRRefl
;; EfCoTotalNatMR
;; TotalNatMRToCoTotalMR

;; EfEqPNat
;; EfEqPNatNc
;; EqPNatNcToEqD
;; EqPNatSym
;; EqPNatNcSym
;; EqPNatRefl
;; EqPNatNcRefl
;; EqPNatToTotalLeft
;; EqPNatNcToTotalNcLeft
;; EqPNatToTotalRight
;; EqPNatNcToTotalNcRight
;; EqPNatNcTrans
;; EqPNatNcToEq
;; EqNatToEqPNc

;; EfCoEqPNat
;; EfCoEqPNatNc
;; CoEqPNatNcToEqD
;; CoEqPNatSym
;; CoEqPNatNcSym
;; CoEqPNatRefl
;; CoEqPNatNcRefl
;; CoEqPNatToCoTotalLeft
;; CoEqPNatNcToCoTotalNcLeft
;; CoEqPNatToCoTotalRight
;; CoEqPNatNcToCoTotalNcRight
;; CoEqPNatNcTrans
;; EqPNatToCoEqP
;; EqPNatNcToCoEqPNc
;; EfEqPNatMR
;; EqPNatMRToEqDLeft
;; EqPNatMRToEqDRight
;; EqPNatNcToTotalMR
;; TotalNatMRToEqPNc
;; EqPNatMRToTotalNc
;; EqPNatMRRefl
;; EqPNatNcToEqPMR
;; EqPNatMRToEqPNcLeft
;; EqPNatMRToEqPNcRight
;; EfCoEqPNatMR
;; EqPNatMRToCoEqPMR
;; CoEqPNatNcToCoTotalMR
;; CoTotalNatMRToCoEqPNc
;; CoEqPNatMRRefl
;; CoEqPNatNcToCoEqPMR
;; CoEqPNatMRToCoEqPNcLeft
;; CoEqPNatMRToCoEqPNcRight

;; EfTotalNat
(set-goal "allnc n^(F -> TotalNat n^)")
(assume "n^" "Absurd")
(simp (pf "n^ eqd 0"))
(use "TotalNatZero")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfTotalNat")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;; 0

;; EfTotalNatNc
(set-goal "allnc n^(F -> TotalNatNc n^)")
(assume "n^" "Absurd")
(simp (pf "n^ eqd 0"))
(use "TotalNatNcZero")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfTotalNatNc")

;; TotalNatToCoTotal
(set-goal "allnc n^(TotalNat n^ -> CoTotalNat n^)")
(assume "n^" "Tn")
(coind "Tn")
(assume "n^1" "Tn1")
(assert "n^1 eqd 0 ori exr n^2(TotalNat n^2 andi n^1 eqd Succ n^2)")
 (elim "Tn1")
 (intro 0)
 (use "InitEqD")
 (assume "n^2" "Tn2" "Useless")
 (intro 1)
 (intro 0 (pt "n^2"))
 (split)
 (use "Tn2")
 (use "InitEqD")
;; Assertion proved.
(assume "Disj")
(elim "Disj")
(assume "n1=0")
(intro 0)
(use "n1=0")
(assume "ExHyp")
(intro 1)
(by-assume "ExHyp" "n^2" "n2Prop")
(intro 0 (pt "n^2"))
(split)
(intro 1)
(use "n2Prop")
(use "n2Prop")
;; Proof finished.
;; (cp)
(save "TotalNatToCoTotal")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

;; [n]
;;  (CoRec nat=>nat)n
;;  ([n0][if n0 (DummyL nat ysum nat) ([n1]Inr((InR nat nat)n1))])

;; TotalNatNcToCoTotalNc
(set-goal "allnc n^(TotalNatNc n^ -> CoTotalNatNc n^)")
(assume "n^" "Tn")
(coind "Tn")
(assume "n^1" "Tn1")
(assert "n^1 eqd 0 ornc exnc n^2(TotalNatNc n^2 andi n^1 eqd Succ n^2)")
 (elim "Tn1")
 (intro 0)
 (use "InitEqD")
 (assume "n^2" "Tn2" "Useless")
 (intro 1)
 (intro 0 (pt "n^2"))
 (split)
 (use "Tn2")
 (use "InitEqD")
;; Assertion proved.
(assume "Disj")
(elim "Disj")
(assume "n1=0")
(intro 0)
(use "n1=0")
(assume "ExHyp")
(intro 1)
(by-assume "ExHyp" "n^2" "n2Prop")
(intro 0 (pt "n^2"))
(split)
(intro 1)
(use "n2Prop")
(use "n2Prop")
;; Proof finished.
;; (cp)
(save "TotalNatNcToCoTotalNc")

;; EfCoTotalNat
(set-goal "allnc n^(F -> CoTotalNat n^)")
(assume "n^" "Absurd")
(coind "Absurd")
(assume "n^1" "Useless")
(intro 0)
(simp (pf "n^1 eqd 0"))
(use "InitEqD")
(simp (pf "n^1 eqd 0"))
(use "InitEqD")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfCoTotalNat")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;; (CoRec nat)(DummyL nat ysumu)

;; EfCoTotalNatNc
(set-goal "allnc n^(F -> CoTotalNatNc n^)")
(assume "n^" "Absurd")
(coind "Absurd")
(assume "n^1" "Useless")
(intro 0)
(simp (pf "n^1 eqd 0"))
(use "InitEqD")
(simp (pf "n^1 eqd 0"))
(use "InitEqD")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfCoTotalNatNc")

;; TotalNatMRToEqD
(set-goal "allnc n^1,n^2(TotalNatMR n^1 n^2 -> n^1 eqd n^2)")
(assume "n^1" "n^2" "TMRn1n2")
(elim "TMRn1n2")
;; 3,4
(use "InitEqD")
;; 4
(assume "n^3" "n^4" "Useless" "EqHyp")
(simp "EqHyp")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "TotalNatMRToEqD")

;; TotalNatMRToTotalNcLeft
(set-goal "allnc n^1,n^2(TotalNatMR n^1 n^2 -> TotalNatNc n^1)")
(assume "n^1" "n^2" "TMRHyp")
(elim "TMRHyp")
;; 3,4
(use "TotalNatNcZero")
;; 4
(assume "n^3" "n^4" "Useless")
(use "TotalNatNcSucc")
;; Proof finished.
;; (cp)
(save "TotalNatMRToTotalNcLeft")

;; TotalNatMRToTotalNcRight
(set-goal "allnc n^1,n^2(TotalNatMR n^1 n^2 -> TotalNatNc n^2)")
(assume "n^1" "n^2" "TMRHyp")
(elim "TMRHyp")
;; 3,4
(use "TotalNatNcZero")
;; 4
(assume "n^3" "n^4" "Useless")
(use "TotalNatNcSucc")
;; Proof finished.
;; (cp)
(save "TotalNatMRToTotalNcRight")

;; TotalNatMRRefl
(set-goal "allnc n^(TotalNat n^ -> TotalNatMR n^ n^)")
(assume "n^" "TMRHyp")
(elim "TMRHyp")
;; 3,4
(use "TotalNatZeroMR")
;; 4
(assume "n^1" "n^1" "TMRn1n1")
(use "TotalNatSuccMR")
(use "TMRn1n1")
;; Proof finished.
;; (cp)
(save "TotalNatMRRefl")

;; EfCoTotalNatMR
(set-goal "allnc n^1,n^2(F -> CoTotalNatMR n^1 n^2)")
(assume "n^1" "n^2" "Absurd")
(coind "Absurd")
(assume "n^3" "n^4" "Useless")
(intro 0)
(simp (pf "n^3 eqd 0"))
(simp (pf "n^4 eqd 0"))
(split)
(use "InitEqD")
(use "InitEqD")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfCoTotalNatMR")

;; TotalNatMRToCoTotalMR
(set-goal "allnc n^1,n^2(TotalNatMR n^1 n^2 -> CoTotalNatMR n^1 n^2)")
(assume "n^1" "n^2" "Tn1n2")
(coind "Tn1n2")
(assume "n^3" "n^4" "Tn3n4")
(assert "n^3 eqd 0 andnc n^4 eqd0 ornc
         exr n^5,n^6(TotalNatMR n^5 n^6 andnc 
        n^3 eqd Succ n^5 andnc
        n^4 eqd Succ n^6)")
 (elim "Tn3n4")
;; 7,8
 (intro 0)
 (split)
 (use "InitEqD")
 (use "InitEqD")
;; 8
 (assume "n^5" "n^6" "Tn5n6" "Useless")
 (drop "Useless")
 (intro 1)
 (intro 0 (pt "n^5"))
 (intro 0 (pt "n^6"))
 (split)
 (use "Tn5n6")
 (split)
 (use "InitEqD")
 (use "InitEqD")
;; Assertion proved.
(assume "Disj")
(elim "Disj")
;; 22,23
(assume "Conj")
(intro 0)
(use "Conj")
;; 23
(drop "Disj")
(assume "ExHyp")
(intro 1)
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 0 (pt "n^5"))
(intro 0 (pt "n^6"))
(split)
(intro 1)
(use "n5n6Prop")
(use "n5n6Prop")
;; Proof finished.
;; (cp)
(save "TotalNatMRToCoTotalMR")

;; EfEqPNat
(set-goal "allnc n^1,n^2(F -> EqPNat n^1 n^2)")
(assume "n^1" "n^2" "Absurd")
(simp (pf "n^1 eqd 0"))
(simp (pf "n^2 eqd 0"))
(use "EqPNatZero")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfEqPNat")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;; 0

;; EfEqPNatNc
(set-goal "allnc n^1,n^2(F -> EqPNatNc n^1 n^2)")
(assume "n^1" "n^2" "Absurd")
(simp (pf "n^1 eqd 0"))
(simp (pf "n^2 eqd 0"))
(use "EqPNatNcZero")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfEqPNatNc")

;; EqPNatNcToEqD
(set-goal "allnc n^1,n^2(EqPNatNc n^1 n^2 -> n^1 eqd n^2)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
;; 3,4
(use "InitEqD")
;; 4
(assume "n^3" "n^4" "Useless" "IH")
(simp "IH")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "EqPNatNcToEqD")

;; EqPNatSym
(set-goal "allnc n^1,n^2(EqPNat n^1 n^2 -> EqPNat n^2 n^1)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
(use "EqPNatZero")
(assume "n^3" "n^4" "Useless" "EqPn4n3")
(use "EqPNatSucc")
(use "EqPn4n3")
;; Proof finished.
;; (cp)
(save "EqPNatSym")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp (rename-variables neterm))
;; [n](Rec nat=>nat)n Zero([n0]Succ)

;; EqPNatNcSym
(set-goal "allnc n^1,n^2(EqPNatNc n^1 n^2 -> EqPNatNc n^2 n^1)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
(use "EqPNatNcZero")
(assume "n^3" "n^4" "Useless" "EqPn4n3")
(use "EqPNatNcSucc")
(use "EqPn4n3")
;; Proof finished.
;; (cp)
(save "EqPNatNcSym")

;; EqPNatRefl
(set-goal "allnc n^(TotalNat n^ -> EqPNat n^ n^)")
(assume "n^" "Tn")
(elim "Tn")
(use "EqPNatZero")
(assume "n^1" "Tn1")
(use "EqPNatSucc")
;; Proof finished.
;; (cp)
(save "EqPNatRefl")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp (rename-variables neterm))
;; [n](Rec nat=>nat)n Zero([n0]Succ)

;; EqPNatNcRefl
(set-goal "allnc n^(TotalNatNc n^ -> EqPNatNc n^ n^)")
(assume "n^" "Tn")
(elim "Tn")
(use "EqPNatNcZero")
(assume "n^1" "Tn1" "EqPHyp")
(use "EqPNatNcSucc")
(use "EqPHyp")
;; Proof finished.
;; (cp)
(save "EqPNatNcRefl")

;; EqPNatToTotalLeft
(set-goal "allnc n^1,n^2(EqPNat n^1 n^2 -> TotalNat n^1)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
;; 3,4
(use "TotalNatZero")
;; 4
(assume "n^3" "n^4" "Useless" "IH")
(use "TotalNatSucc")
(use "IH")
;; Proof finished.
;; (cp)
(save "EqPNatToTotalLeft")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;; [n](Rec nat=>nat)n Zero([n0]Succ)

;; EqPNatNcToTotalNcLeft
(set-goal "allnc n^1,n^2(EqPNatNc n^1 n^2 -> TotalNatNc n^1)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
;; 3,4
(use "TotalNatNcZero")
;; 4
(assume "n^3" "n^4" "EqPn3n4" "IH")
(use "TotalNatNcSucc")
(use "IH")
;; Proof finished.
;; (cp)
(save "EqPNatNcToTotalNcLeft")

;; EqPNatToTotalRight
(set-goal "allnc n^1,n^2(EqPNat n^1 n^2 -> TotalNat n^2)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
;; 3,4
(use "TotalNatZero")
;; 4
(assume "n^3" "n^4" "Useless" "IH")
(use "TotalNatSucc")
(use "IH")
;; Proof finished.
;; (cp)
(save "EqPNatToTotalRight")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;; [n](Rec nat=>nat)n Zero([n0]Succ)

;; EqPNatNcToTotalNcRight
(set-goal "allnc n^1,n^2(EqPNatNc n^1 n^2 -> TotalNatNc n^2)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
;; 3,4
(use "TotalNatNcZero")
;; 4
(assume "n^3" "n^4" "EqPn3n4" "IH")
(use "TotalNatNcSucc")
(use "IH")
;; Proof finished.
;; (cp)
(save "EqPNatNcToTotalNcRight")

;; EqPNatNcTrans
(set-goal
 "allnc n^1,n^2,n^3(EqPNatNc n^1 n^2 -> EqPNatNc n^2 n^3 -> EqPNatNc n^1 n^3)")
(assume "n^1" "n^2" "n^3" "EqPn1n2" "EqPn2n3")
(simp (pf "n^1 eqd n^2"))
(simp (pf "n^2 eqd n^3"))
(use "EqPNatNcRefl")
(use "EqPNatNcToTotalNcRight" (pt "n^2"))
(use "EqPn2n3")
(use "EqPNatNcToEqD")
(use "EqPn2n3")
(use "EqPNatNcToEqD")
(use "EqPn1n2")
;; Proof finished.
;; (cp)
(save "EqPNatNcTrans")

;; EqPNatNcToEq
(set-goal "allnc n^1,n^2(EqPNatNc n^1 n^2 -> n^1=n^2)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
(use "Truth")
(assume "n^13" "n^4" "Useless" "IH")
(use "IH")
;; Proof finished.
;; (cp)
(save "EqPNatNcToEq")

;; EqNatToEqPNc
(set-goal "allnc n^1(TotalNatNc n^1 -> allnc n^2(TotalNatNc n^2 ->
 n^1=n^2 -> EqPNatNc n^1 n^2))")
(assume "n^1" "Tn1")
(elim "Tn1")
;; 3,4
(assume "n^2" "Tn2")
(elim "Tn2")
(assume "Useless")
(use "EqPNatNcZero")
;; 7
(assume "n^3" "Tn3" "Useless" "Absurd")
(use "EfEqPNatNc")
(use "Absurd")
;; 4
(assume "n^2" "Tn2" "IH" "n^3" "Tn3")
(elim "Tn3")
(assume "Absurd")
(use "EfEqPNatNc")
(use "Absurd")
;; 13
(assume "n^4" "Tn4" "Useless" "n2=n4")
(use "EqPNatNcSucc")
(use "IH")
(use "Tn4")
(use "n2=n4")
;; Proof finished.
;; (cp)
(save "EqNatToEqPNc")

;; EfCoEqPNat
(set-goal "allnc n^1,n^2(F -> CoEqPNat n^1 n^2)")
(assume "n^1" "n^2" "Absurd")
(coind "Absurd")
(assume "n^3" "n^4" "Useless")
(intro 0)
(simp (pf "n^3 eqd 0"))
(simp (pf "n^4 eqd 0"))
(split)
(use "InitEqD")
(use "InitEqD")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfCoEqPNat")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;; (CoRec nat)(DummyL nat ysumu)
(pp (nt (undelay-delayed-corec neterm 1)))
;; 0

;; EfCoEqPNatNc
(set-goal "allnc n^1,n^2(F -> CoEqPNatNc n^1 n^2)")
(assume "n^1" "n^2" "Absurd")
(coind "Absurd")
(assume "n^3" "n^4" "Useless")
(intro 0)
(simp (pf "n^3 eqd 0"))
(simp (pf "n^4 eqd 0"))
(split)
(use "InitEqD")
(use "InitEqD")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfCoEqPNatNc")

;; CoEqPNatNcToEqD
(set-goal "allnc n^1,n^2(CoEqPNatNc n^1 n^2 -> n^1 eqd n^2)")
(use (make-proof-in-aconst-form (finalg-to-bisim-aconst (py "nat"))))
;; Proof finished.
;; (cp)
(save "CoEqPNatNcToEqD")

;; CoEqPNatSym
(set-goal "allnc n^1,n^2(CoEqPNat n^1 n^2 -> CoEqPNat n^2 n^1)")
(assume "n^1" "n^2" "n1~n2")
(coind "n1~n2")
(assume "n^3" "n^4" "n4~n3")
(inst-with-to
 (make-proof-in-aconst-form
  (coidpredconst-to-closure-aconst
   (predicate-form-to-predicate (pf "CoEqPNat n^2 n^1"))))
 (pt "n^4") (pt "n^3") "n4~n3" "Inst")
(elim "Inst")
;; 8,9
(drop "Inst")
(assume "Conj")
(intro 0)
(split)
(use "Conj")
(use "Conj")
;; 9
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^6"))
(intro 0 (pt "n^5"))
(split)
(intro 1)
(use "n5n6Prop")
(split)
(use "n5n6Prop")
(use "n5n6Prop")
;; Proof finished.
;; (cp)
(save "CoEqPNatSym")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

;; [n]
;;  (CoRec nat=>nat)n
;;  ([n0][if (Des n0) (DummyL nat ysum nat) ([n1]Inr((InR nat nat)n1))])

;; CoEqPNatNcSym
(set-goal "allnc n^1,n^2(CoEqPNatNc n^1 n^2 -> CoEqPNatNc n^2 n^1)")
(assume "n^1" "n^2" "n1~n2")
(coind "n1~n2")
(assume "n^3" "n^4" "n4~n3")
(inst-with-to
 (make-proof-in-aconst-form
  (coidpredconst-to-closure-aconst
   (predicate-form-to-predicate (pf "CoEqPNatNc n^2 n^1"))))
 (pt "n^4") (pt "n^3") "n4~n3" "Inst")
(elim "Inst")
;; 8,9
(drop "Inst")
(assume "Conj")
(intro 0)
(split)
(use "Conj")
(use "Conj")
;; 9
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^6"))
(intro 0 (pt "n^5"))
(split)
(intro 1)
(use "n5n6Prop")
(split)
(use "n5n6Prop")
(use "n5n6Prop")
;; Proof finished.
;; (cp)
(save "CoEqPNatNcSym")

;; CoEqPNatRefl
(set-goal "allnc n^(CoTotalNat n^ -> CoEqPNat n^ n^)")
(assert "allnc n^1,n^2(CoTotalNat n^1 andi n^1 eqd n^2 -> CoEqPNat n^1 n^2)")
(assume "n^1" "n^2")
(coind)
(assume "n^3" "n^4" "Conj")
(inst-with-to "Conj" 'left "CoTn3")
(inst-with-to "Conj" 'right "n3=n4")
(drop "Conj")
(simp "<-" "n3=n4")
(drop "n3=n4")
(inst-with-to "CoTotalNatClause" (pt "n^3") "CoTn3" "Inst")
(elim "Inst")
;; 16,17
(drop "Inst")
(assume "n3=0")
(intro 0)
(split)
(use "n3=0")
(use "n3=0")
;; 17
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^5"))
(split)
(intro 1)
(split)
(use "n5Prop")
(use "InitEqD")
(split)
(use "n5Prop")
(use "n5Prop")
;; 2
(assume "Assertion" "n^" "CoTn")
(use "Assertion")
(split)
(use "CoTn")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "CoEqPNatRefl")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

;; [n]
;;  (CoRec nat=>nat)n
;;  ([n0][if (Des n0) (DummyL nat ysum nat) ([n1]Inr((InR nat nat)n1))])

;; CoEqPNatNcRefl
(set-goal "allnc n^(CoTotalNatNc n^ -> CoEqPNatNc n^ n^)")
(assert
 "allnc n^1,n^2(CoTotalNatNc n^1 andi n^1 eqd n^2 -> CoEqPNatNc n^1 n^2)")
(assume "n^1" "n^2")
(coind)
(assume "n^3" "n^4" "Conj")
(inst-with-to "Conj" 'left "CoTn3")
(inst-with-to "Conj" 'right "n3=n4")
(drop "Conj")
(simp "<-" "n3=n4")
(drop "n3=n4")
(inst-with-to "CoTotalNatNcClause" (pt "n^3") "CoTn3" "Inst")
(elim "Inst")
;; 16,17
(drop "Inst")
(assume "n3=0")
(intro 0)
(split)
(use "n3=0")
(use "n3=0")
;; 17
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^5"))
(split)
(intro 1)
(split)
(use "n5Prop")
(use "InitEqD")
(split)
(use "n5Prop")
(use "n5Prop")
;; 2
(assume "Assertion" "n^" "CoTn")
(use "Assertion")
(split)
(use "CoTn")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "CoEqPNatNcRefl")

;; CoEqPNatToCoTotalLeft
(set-goal "allnc n^1,n^2(CoEqPNat n^1 n^2 -> CoTotalNat n^1)")
(assume "n^1" "n^2" "n1~n2")
(use (imp-formulas-to-coind-proof
      (pf "exr n^3 CoEqPNat n^1 n^3 -> CoTotalNat n^1")))
;; 3,4
(assume "n^3" "ExHyp3")
(by-assume "ExHyp3" "n^4" "n3~n4")
(inst-with-to "CoEqPNatClause" (pt "n^3") (pt "n^4") "n3~n4" "Inst")
(elim "Inst")
;; 11,12
(drop "Inst")
(assume "Conj")
(intro 0)
(use "Conj")
;; 12
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^5"))
(split)
(intro 1)
(intro 0 (pt "n^6"))
(use "n5n6Prop")
(use "n5n6Prop")
;; 4
(intro 0 (pt "n^2"))
(use "n1~n2")
;; Proof finished.
;; (cp)
(save "CoEqPNatToCoTotalLeft")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

;; [n]
;;  (CoRec nat=>nat)n
;;  ([n0][if (Des n0) (DummyL nat ysum nat) ([n1]Inr((InR nat nat)n1))])

;; CoEqPNatNcToCoTotalNcLeft
(set-goal "allnc n^1,n^2(CoEqPNatNc n^1 n^2 -> CoTotalNatNc n^1)")
(assume "n^1" "n^2" "n1~n2")
(use (imp-formulas-to-coind-proof
      (pf "exr n^3 CoEqPNatNc n^1 n^3 -> CoTotalNatNc n^1")))
;; 3,4
(assume "n^3" "ExHyp3")
(by-assume "ExHyp3" "n^4" "n3~n4")
(inst-with-to "CoEqPNatNcClause" (pt "n^3") (pt "n^4") "n3~n4" "Inst")
(elim "Inst")
;; 11,12
(drop "Inst")
(assume "Conj")
(intro 0)
(use "Conj")
;; 12
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^5"))
(split)
(intro 1)
(intro 0 (pt "n^6"))
(use "n5n6Prop")
(use "n5n6Prop")
;; 4
(intro 0 (pt "n^2"))
(use "n1~n2")
;; Proof finished.
;; (cp)
(save "CoEqPNatNcToCoTotalNcLeft")

;; CoEqPNatToCoTotalRight
(set-goal "allnc n^1,n^2(CoEqPNat n^1 n^2 -> CoTotalNat n^2)")
(assume "n^1" "n^2" "n1~n2")
(use (imp-formulas-to-coind-proof
      (pf "exr n^3 CoEqPNat n^3 n^2 -> CoTotalNat n^2")))
;; 3,4
(assume "n^3" "ExHyp3")
(by-assume "ExHyp3" "n^4" "n4~n3")
(inst-with-to "CoEqPNatClause" (pt "n^4") (pt "n^3") "n4~n3" "Inst")
(elim "Inst")
;; 11,12
(drop "Inst")
(assume "Conj")
(intro 0)
(use "Conj")
;; 12
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^6"))
(split)
(intro 1)
(intro 0 (pt "n^5"))
(use "n5n6Prop")
(use "n5n6Prop")
;; 4
(intro 0 (pt "n^1"))
(use "n1~n2")
;; Proof finished.
;; (cp)
(save "CoEqPNatToCoTotalRight")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

;; [n]
;;  (CoRec nat=>nat)n
;;  ([n0][if (Des n0) (DummyL nat ysum nat) ([n1]Inr((InR nat nat)n1))])

;; CoEqPNatNcToCoTotalNcRight
(set-goal "allnc n^1,n^2(CoEqPNatNc n^1 n^2 -> CoTotalNatNc n^2)")
(assume "n^1" "n^2" "n1~n2")
(use (imp-formulas-to-coind-proof
      (pf "exr n^3 CoEqPNatNc n^3 n^2 -> CoTotalNatNc n^2")))
;; 3,4
(assume "n^4" "ExHyp3")
(by-assume "ExHyp3" "n^3" "n3~n4")
(inst-with-to "CoEqPNatNcClause" (pt "n^3") (pt "n^4") "n3~n4" "Inst")
(elim "Inst")
;; 11,12
(drop "Inst")
(assume "Conj")
(intro 0)
(use "Conj")
;; 12
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^6"))
(split)
(intro 1)
(intro 0 (pt "n^5"))
(use "n5n6Prop")
(use "n5n6Prop")
;; 4
(intro 0 (pt "n^1"))
(use "n1~n2")
;; Proof finished.
;; (cp)
(save "CoEqPNatNcToCoTotalNcRight")

;; CoEqPNatNcTrans
(set-goal "allnc n^1,n^2,n^3(CoEqPNatNc n^1 n^2 -> CoEqPNatNc n^2 n^3 ->
                             CoEqPNatNc n^1 n^3)")
(assume "n^1" "n^2" "n^3" "CoEqPn1n2" "CoEqPn2n3")
(simp (pf "n^1 eqd n^2"))
(simp (pf "n^2 eqd n^3"))
(use "CoEqPNatNcRefl")
(use "CoEqPNatNcToCoTotalNcRight" (pt "n^2"))
(use "CoEqPn2n3")
(use "CoEqPNatNcToEqD")
(use "CoEqPn2n3")
(use "CoEqPNatNcToEqD")
(use "CoEqPn1n2")
;; Proof finished.
;; (cp)
(save "CoEqPNatNcTrans")

;; EqPNatToCoEqP
(set-goal "allnc n^1,n^2(EqPNat n^1 n^2 -> CoEqPNat n^1 n^2)")
(assume "n^1" "n^2" "EqPn1n2")
(coind "EqPn1n2")
(assume "n^3" "n^4" "EqPn3n4")
(elim "EqPn3n4")
;; 5,6
(intro 0)
(split)
(use "InitEqD")
(use "InitEqD")
;; 6
(assume "n^5" "n^6" "EqPn5n6" "Disj")
(elim "Disj")
;; 11,12
(drop "Disj")
(assume "Conj")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^6"))
(split)
(intro 1)
(use "EqPn5n6")
(split)
(use "InitEqD")
(use "InitEqD")
;; 12
(drop "Disj")
(assume "ExHyp")
(by-assume "ExHyp" "n^7" "n7Prop")
(by-assume "n7Prop" "n^8" "n7n8Prop")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^6"))
(split)
(intro 1)
(use "EqPn5n6")
(split)
(use "InitEqD")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "EqPNatToCoEqP")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)

;; [n]
;;  (CoRec nat=>nat)n
;;  ([n0]
;;    (Rec nat=>uysum(nat ysum nat))n0(DummyL nat ysum nat)
;;    ([n1,(uysum(nat ysum nat))]Inr((InR nat nat)n1)))

;; EqPNatNcToCoEqPNc
(set-goal "allnc n^1,n^2(EqPNatNc n^1 n^2 -> CoEqPNatNc n^1 n^2)")
(assume "n^1" "n^2" "EqPn1n2")
(coind "EqPn1n2")
(assume "n^3" "n^4" "EqPn3n4")
(elim "EqPn3n4")
;; 5,6
(intro 0)
(split)
(use "InitEqD")
(use "InitEqD")
;; 6
(assume "n^5" "n^6" "EqPn5n6" "Disj")
(elim "Disj")
;; 11,12
(drop "Disj")
(assume "Conj")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^6"))
(split)
(intro 1)
(use "EqPn5n6")
(split)
(use "InitEqD")
(use "InitEqD")
;; 12
(drop "Disj")
(assume "ExHyp")
(by-assume "ExHyp" "n^7" "n7Prop")
(by-assume "n7Prop" "n^8" "n7n8Prop")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^6"))
(split)
(intro 1)
(use "EqPn5n6")
(split)
(use "InitEqD")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "EqPNatNcToCoEqPNc")

;; EfEqPNatMR
(set-goal "allnc n^1,n^2,n^3(F -> EqPNatMR n^1 n^2 n^3)")
(assume "n^1" "n^2" "n^3" "Absurd")
(simp (pf "n^1 eqd 0"))
(simp (pf "n^2 eqd 0"))
(simp (pf "n^3 eqd 0"))
(use "EqPNatZeroMR")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfEqPNatMR")

;; EqPNatMRToEqDLeft
(set-goal "allnc n^1,n^2,n^3(EqPNatMR n^1 n^2 n^3 -> n^1 eqd n^2)")
(assume "n^1" "n^2" "n^3" "EqPHyp")
(elim "EqPHyp")
(use "InitEqD")
(assume "n^4" "n^5" "n^6" "Useless" "EqDHyp")
(simp "EqDHyp")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "EqPNatMRToEqDLeft")

;; EqPNatMRToEqDRight
(set-goal "allnc n^1,n^2,n^3(EqPNatMR n^1 n^2 n^3 -> n^2 eqd n^3)")
(assume "n^1" "n^2" "n^3" "EqPHyp")
(elim "EqPHyp")
(use "InitEqD")
(assume "n^4" "n^5" "n^6" "Useless" "EqDHyp")
(simp "EqDHyp")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "EqPNatMRToEqDRight")

;; EqPNatNcToTotalMR
(set-goal "allnc n^1,n^2(EqPNatNc n^1 n^2 -> TotalNatMR n^1 n^2)")
(assume "n^1" "n^2" "EqPn1n2")
(elim "EqPn1n2")
(use "TotalNatZeroMR")
(assume "n^3" "n^4" "Useless")
(use "TotalNatSuccMR")
;; Proof finished.
;; (cp)
(save "EqPNatNcToTotalMR")

;; TotalNatMRToEqPNc
(set-goal "allnc n^1,n^2(TotalNatMR n^1 n^2 -> EqPNatNc n^1 n^2)")
(assume "n^1" "n^2" "TMRn1n2")
(elim "TMRn1n2")
(use "EqPNatNcZero")
(assume "n^3" "n^4" "Useless")
(use "EqPNatNcSucc")
;; Proof finished.
;; (cp)
(save "TotalNatMRToEqPNc")

;; EqPNatMRToTotalNc
(set-goal "allnc n^1,n^2,n^3(EqPNatMR n^1 n^2 n^3 -> TotalNatNc n^3)")
(assume "n^1" "n^2" "n^3" "EqPHyp")
(elim "EqPHyp")
(use "TotalNatNcZero")
(assume "n^4" "n^5" "n^6" "Useless")
(use "TotalNatNcSucc")
;; Proof finished.
;; (cp)
(save "EqPNatMRToTotalNc")

;; EqPNatMRRefl
(set-goal "allnc n^(TotalNatNc n^ -> EqPNatMR n^ n^ n^)")
(assume "n^" "Tn")
(elim "Tn")
(use "EqPNatZeroMR")
(assume "n^1" "IH")
(use "EqPNatSuccMR")
;; Proof finished.
;; (cp)
(save "EqPNatMRRefl")

;; EqPNatNcToEqPMR
(set-goal "allnc n^1,n^2,n^3(EqPNatNc n^1 n^2 -> EqPNatNc n^2 n^3 ->
                             EqPNatMR n^1 n^2 n^3)")
(assume "n^1" "n^2" "n^3" "EqPn1n2" "EqPn2n3")
(simp (pf "n^1 eqd n^2"))
(simp (pf "n^2 eqd n^3"))
(use "EqPNatMRRefl")
(use "EqPNatNcToTotalNcRight" (pt "n^2"))
(use "EqPn2n3")
(use "EqPNatNcToEqD")
(use "EqPn2n3")
(use "EqPNatNcToEqD")
(use "EqPn1n2")
;; Proof finished.
;; (cp)
(save "EqPNatNcToEqPMR")

;; EqPNatMRToEqPNcLeft
(set-goal "allnc n^1,n^2,n^3(EqPNatMR n^1 n^2 n^3 -> EqPNatNc n^1 n^2)")
(assume "n^1" "n^2" "n^3" "EqPMRHyp")
(elim "EqPMRHyp")
(use "EqPNatNcZero")
(assume "n^4" "n^5" "n^6" "Useless" "EqPn4n5")
(use "EqPNatNcSucc")
(use "EqPn4n5")
;; Proof finished.
;; (cp)
(save "EqPNatMRToEqPNcLeft")

;; EqPNatMRToEqPNcRight
(set-goal "allnc n^1,n^2,n^3(EqPNatMR n^1 n^2 n^3 -> EqPNatNc n^2 n^3)")
(assume "n^1" "n^2" "n^3" "EqPMRHyp")
(elim "EqPMRHyp")
(use "EqPNatNcZero")
(assume "n^4" "n^5" "n^6" "Useless" "EqPn5n6")
(use "EqPNatNcSucc")
(use "EqPn5n6")
;; Proof finished.
;; (cp)
(save "EqPNatMRToEqPNcRight")

;; EfCoEqPNatMR
(set-goal "allnc n^1,n^2,n^3(F -> CoEqPNatMR n^1 n^2 n^3)")
(assume "n^1" "n^2" "n^3" "Absurd")
(coind "Absurd")
(assume "n^4" "n^5" "n^6" "Useless")
(intro 0)
(simp (pf "n^4 eqd 0"))
(simp (pf "n^5 eqd 0"))
(simp (pf "n^6 eqd 0"))
(split)
(use "InitEqD")
(split)
(use "InitEqD")
(use "InitEqD")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfCoEqPNatMR")

;; EqPNatMRToCoEqPMR
(set-goal "allnc n^1,n^2,n^3(
 EqPNatMR n^1 n^2 n^3 -> CoEqPNatMR n^1 n^2 n^3)")
(assume "n^1" "n^2" "n^3" "Tn1n2n3")
(coind "Tn1n2n3")
(assume "n^4" "n^5" "n^6" "Tn4n5n6")
(assert "n^4 eqd 0 andnc n^5 eqd 0 andnc n^6 eqd 0 ornc
         exr n^7,n^8,n^9(EqPNatMR n^7 n^8 n^9 andnc 
         n^4 eqd Succ n^7 andnc
         n^5 eqd Succ n^8 andnc
         n^6 eqd Succ n^9)")
 (elim "Tn4n5n6")
;; 7,8
 (intro 0)
 (split)
 (use "InitEqD")
 (split)
 (use "InitEqD")
 (use "InitEqD")
;; 8
 (assume "n^7" "n^8" "n^9" "Tn7n8n9" "Useless")
 (drop "Useless")
 (intro 1)
 (intro 0 (pt "n^7"))
 (intro 0 (pt "n^8"))
 (intro 0 (pt "n^9"))
 (split)
 (use "Tn7n8n9")
 (split)
 (use "InitEqD")
 (split)
 (use "InitEqD")
 (use "InitEqD")
;; Assertion proved.
(assume "Disj")
(elim "Disj")
;; 27,28
(assume "Conj")
(intro 0)
(use "Conj")
;; 28
(drop "Disj")
(assume "ExHyp")
(intro 1)
(by-assume "ExHyp" "n^7" "n7Prop")
(by-assume "n7Prop" "n^8" "n7n8Prop")
(by-assume "n7n8Prop" "n^9" "n7n8n9Prop")
(intro 0 (pt "n^7"))
(intro 0 (pt "n^8"))
(intro 0 (pt "n^9"))
(split)
(intro 1)
(use "n7n8n9Prop")
(use "n7n8n9Prop")
;; Proof finished.
;; (cp)
(save "EqPNatMRToCoEqPMR")

;; CoEqPNatNcToCoTotalMR
(set-goal "allnc n^1,n^2(CoEqPNatNc n^1 n^2 -> CoTotalNatMR n^1 n^2)")
(assume "n^1" "n^2" "n1~n2")
(use (make-proof-in-aconst-form
      (imp-formulas-to-gfp-aconst
       (pf "CoEqPNatNc n^1 n^2 -> CoTotalNatMR n^1 n^2"))))
;; 3,4
(use "n1~n2")
;; 4
(assume "n^3" "n^4" "n3~n4")
;; use the closure axiom for CoEqPNat
;; (pp "CoEqPNatNcClause")
(inst-with-to "CoEqPNatNcClause" (pt "n^3") (pt "n^4") "n3~n4"
	      "CoEqPNatNcClauseInst")
(elim "CoEqPNatNcClauseInst")
;; 8,9
(drop "CoEqPNatNcClauseInst")
(assume "Conj")
(intro 0)
(split)
(use "Conj")
(use "Conj")
;; 9
(drop "CoEqPNatNcClauseInst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^6"))
(split)
(intro 1)
(use "n5n6Prop")
(split)
(use "n5n6Prop")
(use "n5n6Prop")
;; Proof finished.
;; (cp)
(save "CoEqPNatNcToCoTotalMR")

;; CoTotalNatMRToCoEqPNc
(set-goal "allnc n^1,n^2(CoTotalNatMR n^1 n^2 -> CoEqPNatNc n^1 n^2)")
(assume "n^1" "n^2" "CoTn1n2")
(use (make-proof-in-aconst-form
      (imp-formulas-to-gfp-aconst
       (pf "CoTotalNatMR n^1 n^2 -> CoEqPNatNc n^1 n^2"))))
;; 3,4
(use "CoTn1n2")
;; 4
(assume "n^3" "n^4" "CoTn3n4")
;; use the closure axiom for CoTotalNatMR
(inst-with-to "CoTotalNatMRClause" (pt "n^3") (pt "n^4") "CoTn3n4"
	      "CoTotalNatMRClauseInst")
(elim "CoTotalNatMRClauseInst")
;; 8,9
(drop "CoTotalNatMRClauseInst")
(assume "EqConj")
(intro 0)
(split)
(use "EqConj")
(use "EqConj")
;; 9
(drop "CoTotalNatMRClauseInst")
(assume "ExHyp")
(by-assume "ExHyp" "n^5" "n5Prop")
(by-assume "n5Prop" "n^6" "n5n6Prop")
(intro 1)
(intro 0 (pt "n^5"))
(intro 0 (pt "n^6"))
(split)
(intro 1)
(use "n5n6Prop")
(split)
(use "n5n6Prop")
(use "n5n6Prop")
;; Proof finished.
;; (cp)
(save "CoTotalNatMRToCoEqPNc")

;; CoEqPNatMRRefl
(set-goal "allnc n^(CoTotalNatNc n^ -> CoEqPNatMR n^ n^ n^)")
(assert
 "allnc n^1,n^2,n^3(CoTotalNatNc n^1 andnc n^1 eqd n^2 andnc n^2 eqd n^3 ->
                    CoEqPNatMR n^1 n^2 n^3)")
(assume "n^1" "n^2" "n^3")
(coind)
(assume "n^4" "n^5" "n^6" "Conj")
(inst-with-to "Conj" 'left "CoTn4")
(inst-with-to "Conj" 'right "Conj34")
(inst-with-to "Conj34" 'left "n4=n5")
(inst-with-to "Conj34" 'right "n5=n6")
(drop "Conj" "Conj34")
(simp "<-" "n5=n6")
(simp "<-" "n4=n5")
(drop "n5=n6" "n4=n5")
(inst-with-to "CoTotalNatNcClause" (pt "n^4") "CoTn4" "Inst")
(elim "Inst")
;; 20,21
(drop "Inst")
(assume "n4=0")
(intro 0)
(split)
(use "n4=0")
(split)
(use "n4=0")
(use "n4=0")
;; 21
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^7" "n7Prop")
(intro 1)
(intro 0 (pt "n^7"))
(intro 0 (pt "n^7"))
(intro 0 (pt "n^7"))
(split)
(intro 1)
(split)
(use "n7Prop")
(split)
(use "InitEqD")
(use "InitEqD")
(split)
(use "n7Prop")
(split)
(use "n7Prop")
(use "n7Prop")
;; 2
(assume "Assertion" "n^" "CoTn")
(use "Assertion")
(split)
(use "CoTn")
(split)
(use "InitEqD")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "CoEqPNatMRRefl")

;; CoEqPNatNcToCoEqPMR
(set-goal "allnc n^1,n^2,n^3(CoEqPNatNc n^1 n^2 -> CoEqPNatNc n^2 n^3 ->
                             CoEqPNatMR n^1 n^2 n^3)")
(assume "n^1" "n^2" "n^3" "CoEqPn1n2" "CoEqPn2n3")
(simp (pf "n^1 eqd n^2"))
(simp (pf "n^2 eqd n^3"))
(use "CoEqPNatMRRefl")
(use "CoEqPNatNcToCoTotalNcRight" (pt "n^2"))
(use "CoEqPn2n3")
(use "CoEqPNatNcToEqD")
(use "CoEqPn2n3")
(use "CoEqPNatNcToEqD")
(use "CoEqPn1n2")
;; Proof finished.
;; (cp)
(save "CoEqPNatNcToCoEqPMR")

;; CoEqPNatMRToCoEqPNcLeft
(set-goal "allnc n^1,n^2,n^3(CoEqPNatMR n^1 n^2 n^3 -> CoEqPNatNc n^1 n^2)")
(assume "n^1" "n^2" "n^3" "CoEqPMRn1n2n3")
(use (imp-formulas-to-coind-proof
      (pf "exr n^3 CoEqPNatMR n^1 n^2 n^3 -> CoEqPNatNc n^1 n^2")))
;; 3,4
(assume "n^4" "n^5" "ExHyp45")
(by-assume "ExHyp45" "n^6" "CoEqPMRn4n5n6")
;; (pp "CoEqPNatMRClause")
(inst-with-to "CoEqPNatMRClause"
	      (pt "n^4") (pt "n^5") (pt "n^6") "CoEqPMRn4n5n6" "Inst")
(elim "Inst")
;; 11,12
(drop "Inst")
(assume "Conj")
(intro 0)
(split)
(use "Conj")
(use "Conj")
;; 12
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^7" "n7Prop")
(by-assume "n7Prop" "n^8" "n7n8Prop")
(by-assume "n7n8Prop" "n^9" "n7n8n9Prop")
(intro 1)
(intro 0 (pt "n^7"))
(intro 0 (pt "n^8"))
(split)
(intro 1)
(intro 0 (pt "n^9"))
(use "n7n8n9Prop")
(split)
(use "n7n8n9Prop")
(use "n7n8n9Prop")
;; 4
(intro 0 (pt "n^3"))
(use "CoEqPMRn1n2n3")
;; Proof finished.
;; (cp)
(save "CoEqPNatMRToCoEqPNcLeft")

;; CoEqPNatMRToCoEqPNcRight
(set-goal "allnc n^1,n^2,n^3(CoEqPNatMR n^1 n^2 n^3 -> CoEqPNatNc n^2 n^3)")
(assume "n^1" "n^2" "n^3" "CoEqPMRn1n2n3")
(use (imp-formulas-to-coind-proof
      (pf "exr n^1 CoEqPNatMR n^1 n^2 n^3 -> CoEqPNatNc n^2 n^3")))
;; 3,4
(assume "n^5" "n^6" "ExHyp56")
(by-assume "ExHyp56" "n^4" "CoEqPMRn4n5n6")
;; (pp "CoEqPNatMRClause")
(inst-with-to "CoEqPNatMRClause"
	      (pt "n^4") (pt "n^5") (pt "n^6") "CoEqPMRn4n5n6" "Inst")
(elim "Inst")
;; 11,12
(drop "Inst")
(assume "Conj")
(intro 0)
(split)
(use "Conj")
(use "Conj")
;; 12
(drop "Inst")
(assume "ExHyp")
(by-assume "ExHyp" "n^7" "n7Prop")
(by-assume "n7Prop" "n^8" "n7n8Prop")
(by-assume "n7n8Prop" "n^9" "n7n8n9Prop")
(intro 1)
(intro 0 (pt "n^8"))
(intro 0 (pt "n^9"))
(split)
(intro 1)
(intro 0 (pt "n^7"))
(use "n7n8n9Prop")
(split)
(use "n7n8n9Prop")
(use "n7n8n9Prop")
;; 4
(intro 0 (pt "n^1"))
(use "CoEqPMRn1n2n3")
;; Proof finished.
;; (cp)
(save "CoEqPNatMRToCoEqPNcRight")

;; This concludes the correction of properties of TotalNat and EqPNat.

;; Program constants.

(add-program-constant "NatPlus" (py "nat=>nat=>nat"))
(add-program-constant "NatTimes" (py "nat=>nat=>nat"))
(add-program-constant "NatLt" (py "nat=>nat=>boole"))
(add-program-constant "NatLe" (py "nat=>nat=>boole"))
(add-program-constant "Pred" (py "nat=>nat"))
(add-program-constant "NatMinus" (py "nat=>nat=>nat"))
(add-program-constant "NatMax" (py "nat=>nat=>nat"))
(add-program-constant "NatMin" (py "nat=>nat=>nat"))
(add-program-constant "AllBNat" (py "nat=>(nat=>boole)=>boole"))
(add-program-constant "ExBNat" (py "nat=>(nat=>boole)=>boole"))
(add-program-constant "NatLeast" (py "nat=>(nat=>boole)=>nat"))
(add-program-constant "NatLeastUp" (py "nat=>nat=>(nat=>boole)=>nat"))

;; Tokens used by the parser.

(define (add-nat-tokens)
  (let* ((make-type-string
	  (lambda (type op-string type-strings)
	    (let* ((string (type-to-string type))
		   (l (string->list string)))
	      (if (member string type-strings)
		  (list->string (cons (char-upcase (car l)) (cdr l)))
		  (myerror op-string "unexpected type" type)))))
	 (tc ;term-creator
	  (lambda (op-string . type-strings)
	    (lambda (x y)
	      (let* ((type (term-to-type x))
		     (type-string
		      (make-type-string type op-string type-strings))
		     (internal-name (string-append type-string op-string)))
		(mk-term-in-app-form
		 (make-term-in-const-form
		  (pconst-name-to-pconst internal-name))
		 x y))))))
    (add-token "+" 'add-op (tc "Plus" "nat"))
    (add-token "*" 'mul-op (tc "Times" "nat"))
    (add-token "<" 'rel-op (tc "Lt" "nat"))
    (add-token "<=" 'rel-op (tc "Le" "nat"))
    (add-token "--" 'add-op (tc "Minus" "nat"))
    (add-token "max" 'mul-op (tc "Max" "nat"))
    (add-token "min" 'mul-op (tc "Min" "nat"))))

(add-nat-tokens)

;; (add-nat-display) updates DISPLAY-FUNCTIONS, so that it uses the
;; tokens introduced by (add-nat-tokens).

(define (add-nat-display)
  (let ((dc ;display-creator
	 (lambda (name display-string token-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=? name (const-to-name
					(term-in-const-form-to-const op)))
			(= 2 (length args)))
		   (list token-type display-string
			 (term-to-token-tree (term-to-original (car args)))
			 (term-to-token-tree (term-to-original (cadr args))))
		   #f))))))
    (add-display (py "nat") (dc "NatPlus" "+" 'add-op))
    (add-display (py "nat") (dc "NatTimes" "*" 'mul-op))
    (add-display (py "boole") (dc "NatLt" "<" 'rel-op))
    (add-display (py "boole") (dc "NatLe" "<=" 'rel-op))
    (add-display (py "nat") (dc "NatMinus" "--" 'add-op))
    (add-display (py "nat") (dc "NatMax" "max" 'mul-op))
    (add-display (py "nat") (dc "NatMin" "min" 'mul-op))))

(add-nat-display)

;; (remove-nat-tokens) removes all tokens and from DISPLAY-FUNCTIONS
;; all items (nat proc).

(define (remove-nat-tokens)
  (remove-token "+")
  (remove-token "*")
  (remove-token "<")
  (remove-token "<=")
  (remove-token "--")
  (remove-token "max")
  (remove-token "min")
  (set! DISPLAY-FUNCTIONS
	(list-transform-positive DISPLAY-FUNCTIONS
	  (lambda (item)
	    (not (equal? (car item) (py "nat")))))))

;; NatEqToEqD
(set-goal "all n,m(n=m -> n eqd m)")
(ind)
(cases)
(assume "Useless")
(use "InitEqD")
(assume "n" "0=Sn")
(use "EfEqD")
(use "0=Sn")
(assume "n" "IH")
(cases)
(assume "Sn=0")
(use "EfEqD")
(use "Sn=0")
(assume "m" "Sn=Sm")
(assert "n eqd m")
 (use "IH")
 (use "Sn=Sm")
(assume "n=m")
(elim "n=m")
(strip)
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "NatEqToEqD")

;; Computation rules for the program constants.

;; For NatPlus
(add-computation-rules
 "n+0" "n"
 "n+Succ m" "Succ(n+m)")

(set-totality-goal "NatPlus")
(fold-alltotal)
(assume "n")
(fold-alltotal)
(ind)
;; 5,6
(use "TotalVar")
;; 6
(assume "m" "IH")
(ng #t)
(use "TotalNatSucc")
(use "IH")
;; Proof finished.
;; (cp)
(save-totality)