;;; file hao_suc.scm





(display"

Begin of hao_suc.scm

")



(display"

Extraction of successor function

succ(α,β) :≡  ∀γ. α<β ∧  (γ≺β → γ≼α)

S: ∀α ∃β succ(α,β)

")


(begin

(define (succ var1 var2)
  (string-append "all ord." var1 " ≺ " var2 " ∧ ( ord ≺ " var2 " → ord ≼ " var1 ")"))


(sg "ex ord2." (succ "ord1" "ord2"))
(ind); on ord1
   (ex-intro (pt"①"))
   (cases)
   (use "Truth-Axiom")
   (search)
(assume "ord11" "ord12" "IH11" "IH12")

; let ord be ord12's successor
(by-assume-with "IH12" "ord" "IH12ord")
(drop "IH11" "IH12")

; OP ord11 ord is successor of OP ord11 ord12
(ex-intro (pt"OP ord11 ord"))

; we have to show the successor properties
(ng #t)
(simp-with "IH12ord" (pt "ord") 'left)
(ng #t)
(ind)
   (use "Truth-Axiom")
(assume "ord31" "ord32")
(ng #t)

(cd "ord31 ≺ ord11" "31<11")
(simp(pf "(ord11 ≺ ord31)=F"))
(search)
(use "BooleImp" (pt"ord31≺ord11"))
(auto)

; ?_19: (ord31≺ord11 -> F) ->...
(assume "31≮11")
(ng #t)
(cd "ord11 ≺ ord31" "11<31")
   (ng #t)
   (assume "(*)" "(**)")
   (use-with "IH12ord" (pt"OP ord31 ord32") 'right)
(assume "11≮31" "(*)" "(**)")
(ng #t)
(use-with "IH12ord" (pt"ord32") 'right)
; Proof finished.
(save "S")
(display-theorems "S")
(add-theorem "S_Soundness"
	     (np(proof-to-soundness-proof 
		 (theorem-name-to-proof "S"))))
;(display-theorems "S_Soundness")

(define (succsimp)
  (simp(pf"all ord.(Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord=cS ord")))

(test-extracted-unary "S")

)




(display "
Some RW-rules involving the Successor function

")

(begin

(animate "S")


(sg "(cS ord= ø)=False")
(cases)
(auto)
; Proof finished.
(trw "¬(cS ord= ø)")
(trw "¬(ø = cS ord)")
(trw "¬((Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord= ø)")
(trw "¬(ø =(Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord)")


(display"
α ≺ Sα
")
(sg "ord ≺ cS ord")
(assume "ord")
(use-with "S_Soundness" (pt"ord")(pt "ord"))
; Proof finished.
(deanimate "S")
(trw "ord ≺ cS ord")
(trw "ord≺(Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord")



(display"
Sα ⊀ α
")
(sg"ord≼cS ord")
(assume "ord")
(use "BooleImp" (pt "ord ≺ cS ord"))
(use (pf"all ord1,ord2.ord1≺ord2→ord1≼ord2"))
(auto)
; Proof finished.
(nrw "ord≼cS ord")
(nrw "ord≼(Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord")



(animate "S")

(sg "(OPøord ≺ cS ord)=(ω ≼ ord)")
(ind)
  (use "Truth-Axiom")
(assume "ord1" "ord2" "IH1" "IH2")
(ng #t)
(cds "ord1= ø" "1=0")
  (use "IH2")
(assume "1≠0")
(use "Truth-Axiom")
; Proof finished.
(arw "OPøord ≺ cS ord"  "ω ≼ ord")
(arw "OPøord ≺ ((Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord)"
     "ω ≼ ord")



(sg "OPøord≼cS ord")
(ind)
  (use "Truth-Axiom")
(cases)
(cases)
(auto)
; Proof finished.
(nrw "OPøord≼cS ord")
(nrw "OPøord≼(Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord")





(sg "(ord~cS(OP ord1 ord2)) = (ord~OP ord1 (cS ord2))")
(search)
; Proof finished.
(arw "ord~cS(OP ord1 ord2)" "ord~OP ord1 (cS ord2)")
(arw "ord~OP ord1((Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2)" 
     "ord~OP ord1 (cS ord2)")


(sg "(cS ord1 ≺ OP (OP ord3 ord4) ø)=(ord1 ≺ OP (OP ord3 ord4) ø)")
(ind)
  (search)
(assume "ord11" "ord12" "IH11" "IH12" "ord3" "ord4")
(ng #t)
(cd "ord11≺OP ord3 ord4" "11<3 4")
(use "IH12")
(search)
; Proof finished.
(arw "cS ord1 ≺ OP (OP ord3 ord4) ø"  "ord1 ≺ OP (OP ord3 ord4) ø")
(arw "(Rec ord=>ord)①([ord2,ord3,ord4]OP ord2)ord1 ≺ OP (OP ord3 ord4) ø"
     "ord1 ≺ OP (OP ord3 ord4) ø")




(sg "(cS ord ~ OP ø ord) = (ord ≺ ω)")
(ind)
    (search)
(assume "ord1" "ord2" "IH1" "IH2")
(ng #t)
(cds "ord1= ø" "1=0")
(auto)
; Proof finished.
(arw "cS ord ~ OP ø ord"  "ord ≺ ω")
(arw "(Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord  ~ OP ø  ord"
     "ord ≺ ω")



(sg "ord ≺ ω → OP ø ord = cS ord")
(ind)
    (search)
(assume "ord1" "ord2" "IH1" "IH2")
(ng #t)
(cds "ord1= ø" "1=0")
(auto)
; Proof finished.
(nrw "ord ≺ ω → OP ø ord = cS ord")
(nrw "ord≺ ω →OPøord=(Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord")



(sg "(OP ord1 ø ~ cS ord2)=(ord1= ø ∧ ord2= ø)")

(ind)
  (search)
(assume "ord21" "ord22" "IH21" "IH22" "ord1")
(ng #t)
(cd "ord21≺ord1" "21<1")
  (ng #t)
  (simp (pf"(ord1≺ord21)=F"))
  (ng #t)
  (cd
     "(OP ord1ø ≼(Rec ord=>ord)①([ord23,ord24,ord25]OP ord23)ord22
   ∧(Rec ord=>ord)①([ord23,ord24,ord25]OP ord23)ord22≼OP ord1ø)"
   "equal")
  (ng #t)
  (simp (pf"F=(ord21≺ord1)"))
  (use "21<1")
  (simp (pf"ord1= ø"))
  (use "Truth-Axiom")
  (booleimp "ord1= ø ∧ord22= ø")
  (use "Truth-Axiom")
  (simp-with "<-" "IH22" (pt"ord1"))
  (use "equal")
  (search)
  (booleimp "ord21≺ord1")
  (auto)
; Proof finished.
(arw  "OP ord1 ø ~ cS ord2"   "ord1= ø ∧ ord2= ø")
(arw  " OP ord1ø ≼(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2
         ∧ (Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2≼OP ord1ø"
      "ord1= ø ∧ ord2= ø")
(arw  "cS ord2 ~ OP ord1 ø" "ord1= ø ∧ ord2= ø")
(arw  "  (Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2≼OP ord1ø
        ∧ OP ord1ø ≼(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2"
      "ord1= ø ∧ ord2= ø")


(sg "¬(OP ord1ø ~cS(OP ord2 ord3))")
(assume "ord2" "ord3" "ord1")
(simp (pf"all ord1,ord2.(OP ord1 ø ~ cS ord2)=(ord1= ø ∧ ord2= ø)"))
(auto)
; Proof finished.
(nrw "¬(OP ord1ø ~cS(OP ord2 ord3))")
(nrw "¬(¬[if (ord≺ord1) (¬(ord1= ø)) False]∧ ¬[if (ord1≺ord) True [if (ord≺ord1) False True]])")
(nrw "¬(cS(OP ord2 ord3) ~ OP ord1ø)")
(nrw "¬(  ¬[if (ord1≺ord2) True
                           [if (ord2≺ord1) (OP ord1ø ≺(Rec ord=>ord)①([ord4,ord5,ord6]OP ord4)ord3) True]]
       ∧ ¬[if (ord2≺ord1) ((Rec ord=>ord)①([ord4,ord5,ord6]OP ord4)ord3≺OP ord1ø) False])")


(deanimate "S")

(sg "ord1≺cS ord2∨ord2≺ord1")
(assume "ord1" "ord2")
(use-with (pf"all ord1,ord2,ord3.ord1≺ord2∧ord2≼ord3→ord1≺ord3")
		  (pt"ord2") (pt"cS ord2") (pt"ord1"))
(search)
; Proof finished.
(nrw "ord1≺cS ord2∨ord2≺ord1")
(nrw "ord1≺(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2∨ord2≺ord1")



(animate "S")

(sg "(ord1≺cS ord2)=(ord1≼ord2)")
(assume "ord1" "ord2")
(cd "ord1≺cS ord2" "1<2+1")
(simp "BooleTrueLeft")
(booleimp "ord1≺cS ord2")
(use "S_Soundness")
(use "1<2+1")
(assume "1≮2+1")
(simp "BooleFalseLeft")
(ng #t)
(booleimp "ord2≺cS ord2 ∧ cS ord2≼ord1")
(use "Truth-Axiom")
(simp "1≮2+1")
(use "Truth-Axiom")
; Proof finished.
(arw "ord1≺cS ord2" "ord1≼ord2")
(arw "ord1≺(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2" "ord1≼ord2")



(deanimate "S")


(sg "ord1≺OP ord2 ø ∧ord2≼ord3→ord1≺OP(cS ord3)ø")
(assume "ord1" "ord2" "ord3")
(use-with "ordSmallerTrans"
		  (pt"ord1") (pt"ω^ord2") (pt"ω^(cS ord3)"))
; Proof finished.
(nrw "(ord1≺OP ord2 ø ∧ ord2≼ord3) → ord1≺OP(cS ord3)ø")
(nrw "(ord1≺OP ord2 ø ∧ ord2≼ord3)
    → ord1≺OP((Rec ord=>ord)①([ord4,ord5,ord6]OP ord4)ord3)ø")


(sg "ord1≼cS ord2∧ord2≺ord1∧ord2≺ ω →ord1~OPøord2")
(assume "ord2" "ord1")
(ass "(*)")
(simp (pf "OPøord2 = cS ord2"))
(ng)
(use-with "(*)" 'left)
(booleimp "ord2≺ ω")
(use "Truth-Axiom")
(use-with "(*)" 'right)
; Proof finished.
(nrw "ord1≼cS ord2∧ord2≺ord1∧ord2≺ ω →ord1~OPøord2")
(nrw "ord1≼(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord2∧ord2≺ord1∧ord2≺ ω
       → ord1~OPøord2")



(sg "(cS ord1≺ ω^ ord2)=(¬(ord2= ø) ∧ ord1≺ ω^ ord2)")
(assume "ord1")
(cases)
   (ng #t)   
   (simp "BooleFalseRight")
(auto)
; Proof finished.
(arw "cS ord1≺ ω^ ord2" "¬(ord2= ø) ∧ ord1≺ ω^ ord2")
(arw "(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord1≺OP ord2ø"
	 "¬(ord2= ø) ∧ ord1≺ ω^ ord2")


(set! COMMENT-FLAG #f)

(display"

End of cS RW-rules

")
)


; Thms

(animate "S")

(display "

FinSucc:  (Sn=1+n) = (n≺ω)

")

(begin

(sg"(cS ord = OP ø ord) = (ord ≺ ω)")
(ind)
  (use "Truth-Axiom")
(assume "ord1" "ord2" "IH1" "IH2")
(ng #t)
(cds "ord1= ø" "1=0")
(auto)
; Proof finished.
(save "FinSucc")
(display-theorems "FinSucc")
)





(display"

Extraction of
Extended Predecessor THM

∀α ∃β,p .  (¬p → (α=ωβ) ∧ p→(α=Sβ))

(takes a while !)
")


(time(begin

(sg "ex ord0,boole.(¬boole → (ord ~ ω⋆ord0)) ∧ (boole→ (ord ~ (cS ord0)))")
(ind)

; ord = 0

(ex-intro(pt"ø"))
(ex-intro(pt"False"))
(use "Truth-Axiom")

; Induction step

(alternate_quants)

(cases)
  (assume "ord1"  "IH1" "IH₀")
  (drop "IH₀")
  (alternate_quants)

; ord=ω^ord1
  (cds "ord1= ø" "1=0")
    (drop  "IH1")
    (ex-intro(pt"True"))
    (ex-intro(pt"ø"))
    (use "Truth-Axiom")
  (assume "1≠0")
  (ng #t)
  (simp "1≠0")
  (ex-intro(pt"False"))
  (ng #t)
  (cd "ord1 ≺ ω" "1<w")
     (by-assume-with "IH1" "ord" "IH1α")
     (ca "ord1~cS ord" "1=Sα")
     (ca "ord ≺ ω" "α<w")
     (ex-intro(pt"OP ord ø"))
     (ng #t)
     (booleimp "ord1~cS ord ∧ cS ord~OPøord")
     (use (pf "all ord1,ord2,ord3. ord1~ord2∧ord2~ord3→ord1~ord3"))
     (strip)
     (use "Truth-Axiom")
     (simp "1=Sα")
     (use "α<w")
     (trans "ord1")
     (simp "1<w")
     (ng "1=Sα" #t)
     (booleimp "ord≺cS ord ∧ cS ord≼ord1")
     (use (pf "all ord1,ord2,ord3. ord1≺ord2∧ord2≼ord3→ord1≺ord3"))
     (strip)
     (use "Truth-Axiom")
     (ng #t)
     (use-with  "1=Sα" 'right)
     (ex-elim "IH1α")
     (cases)
       (search)
     (simp (pf"(ord1~ ω⋆ord)=False"))
     (use "Efq-Atom")
     (simp "BooleFalseRight")
     (booleimp "¬(ord1= ø) ∧ ord1≺ ω")
     (use "Truth-Axiom")
     (simp "1≠0")
     (use "1<w")
  (assume "1≮w")
  (drop "IH1")
  (ex-intro (pt"OP ord1ø"))
  (ng #t)
  (simp "1≮w")
  (use "Truth-Axiom")

(assume "ord21" "ord22" "ord1" "IH1" "IH2")
(by-assume-with "IH2" "ord" "IH2α")
(by-assume-with "IH2α" "p" "IH2αp")
(cd "p" "SORD")
  (ex-intro(pt"OP ord1 ord"))
  (ex-intro(pt"T"))
  (simp(pf"OP ord1(OP ord21 ord22)~cS(OP ord1 ord)"))
  (use "Truth-Axiom")
  (booleimp "p")
  (use-with "IH2αp" 'right)
  (use "SORD")
(assume "¬p")
(ca "OP ord21 ord22~ ω⋆ord" "21,22=wα")
(drop "IH2αp")
(alternate_quants)
(ex-intro(pt"F"))
(ng #t)
(cds "ord1 = ø" "1=0")
  (drop "IH1")
  (ex-intro(pt"ord"))
  (simp(pf"(OPø(OP ord21 ord22)~ ω⋆ord)=(OP ord21 ord22~ ω⋆ord)"))
  (use "21,22=wα")
  (booleimp "OPø(OP ord21 ord22)~ OP ord21 ord22")
  (use (pf"all ord1,ord2,ord3.ord1~ord2 → (ord1~ord3)=(ord2~ord3)"))
  (strip)
  (use "Truth-Axiom")
  (ng)
  (booleimp "OP ord21 ord22~ ω⋆ord")
  (cds "ord21= ø" "21=0")
    (use "Truth-Axiom")
    (search)
  (use "21,22=wα")
(assume "1≠0")
(cd "ord1 ≺ ω" "1<w")
  (by-assume-with "IH1"  "ord4"  "IH1β")
  (ex-intro(pt"OP ord4 ord"))
  (ng #t)
  (ca "ord1~cS ord4" "1=S4")
  (simp(pf "(OPøord4≺ord1)=F"))
  (simp(pf "(ord1≺OPøord4)=F"))
  (ng #t)
  (use "21,22=wα")
  (simp "BooleFalseRight")
  (booleimp "OPøord4≼cS ord4∧cS ord4≼ord1")
  (use(pf"all ord1,ord2,ord3.ord1≼ord2∧ord2≼ord3→ord1≼ord3"))
  (strip)
  (use "Truth-Axiom")
  (use-with "1=S4" 'right)
  (simp "BooleFalseRight")
  (booleimp "ord1≼cS ord4∧ cS ord4≼OPøord4")
  (use(pf"all ord1,ord2,ord3.ord1≼ord2∧ord2≼ord3→ord1≼ord3"))
  (strip)
  (use "Truth-Axiom")
  (simp-with "1=S4" 'left)
  (ng #t)
  (trans "ord1")
  (simp "1<w")
  (ng #t)
  (booleimp "ord4≺cS ord4 ∧ cS ord4≼ord1")
  (use(pf"all ord1,ord2,ord3.ord1≺ord2∧ord2≼ord3→ord1≺ord3"))
  (strip)
  (use "Truth-Axiom")
  (use-with "1=S4" 'right)
  (ex-elim "IH1β")
  (cases)
     (ng #t)
     (search)
  (ng #t)
  (simp(pf"(ord1~ ω⋆ord4)=F"))
  (use "Efq-Atom")
  (simp "BooleFalseRight")
  (cases (pt"ω⋆ord4≺ord1"))
     (search)
  (assume "w4≮1")
  (ng #t)
  (booleimp "(¬(ord1= ø) ∧ ord1≺ ω) ∧ ord1≼ ω⋆ ord4")
  (use "Truth-Axiom")
  (simp "1≠0")
  (simp "w4≮1")
  (use "1<w")
(assume "1≮w")
(ex-intro(pt"OP ord1 ord"))
(ng #t)
(simp(pf "(ord1 ≺ ω)=F"))
(ng #t)
(use "21,22=wα")
(simp "1≮w")
(use "Truth-Axiom")
(booleimp "p∨OP ord21 ord22~ ω⋆ord")
(simp "¬p")
(use "Truth-Axiom")
(use-with "IH2αp" 'left)
; Proof finished.
(save "Pred")
(display-theorems "Pred")


(test-extracted-unary "Pred")

))




(display"

Extraction of predecessor function P from

THM: (∃ξ) ∀nc η. ( α=ξ → cS(η)<α) ∧  (α≠ξ → α=cS(ξ))


")


(begin

(sg "all ord1 ex ord2 allnc ord.
     ((ord1=ord2 → (ord1= ø ∨ ord1≼ord ∨ cS(ord) ≺ ord1)) ∧ (¬(ord1=ord2) → ord1= cS ord2))")
(ca "all ord (Rec ord=>ord)①([ord0,ord1,ord2]OP ord0)ord=cS ord" "succsimp")
(ind)
    (ex-intro(pt"ø"))
    (search)
(assume "ord1" "ord2" "IH1" "IH2")
(drop "IH1")
(cd "ord1= ø ∧ord2= ø" "1,2=1")
    (drop "IH2" "succsimp")
    (ex-intro(pt"ø"))
    (assume "ord")
    (simp-with "1,2=1" 'left)
    (simp-with "1,2=1" 'right)
    (use "Truth-Axiom")
(assume "1,2≠1")
(by-assume-with "IH2" "ord0" "IH2α")
(ex-intro(pt"OP ord1 ord0"))
(ng #t)
(simp-with "IH2α" (pt "OP ord1 ord0") 'right)
(cd "ord2=ord0" "2=0")
(ng #t)
(cds "ord2= ø" "2=NULL")
	(ng #t)
    (assume "ord")
	(booleimp "¬(ord1= ø)")
	(use "Truth-Axiom")
	(use "BooleNegationTwo")
	(assume "1=0")
	(use "1,2≠1")
	(simp "1=0")
	(use "2=NULL")
(assume "2≠0")

; ? allnc ord ord≺OP ord1 ord2→(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord≺OP ord1 ord2 from
(cut(pf"all ord.ord≺OP ord1 ord2→(Rec ord=>ord)①([ord3,ord4,ord5]OP ord3)ord≺OP ord1 ord2"))
(search)
(ind)
	(drop "succsimp" "1,2≠1" "IH2α" "2=0")
	(ng #t)
	(simp "2≠0")
	(use "Truth-Axiom")
(assume "ord3" "ord4" "IH3" "IH4")
(drop "IH3")
(ng #t)
(cd "ord3≺ord1" "3<1")
	(ng #t)
	(use "IH4")
(drop "IH4")
(assume "3≮1")
(ng #t)
(cd "ord1≺ord3" "1<3")
	(ng #t)
	(booleimp "(ord2=ord0→ord2= ø ∨ord2≼(OP ord3 ord4)∨cS (OP ord3 ord4)≺ord2)")
	(simp "2=0")
	(simp "2≠0")
	(use "Truth-Axiom")
	(use-with "IH2α" (pt "OP ord3 ord4") 'left)
(assume "1≮3")
(ng #t)
(booleimp "(ord2=ord0→ord2= ø ∨ord2≼ord4∨cS ord4≺ord2)")
(simp "2=0")
(simp "2≠0")
(use "Truth-Axiom")
(use-with "IH2α" (pt "ord4") 'left)
(auto)
; Proof finished.
(save "P")
(display-theorems "P")

(test-extracted-unary "P")

(add-theorem "P_Soundness"
	     (np(proof-to-soundness-proof 
		 (theorem-name-to-proof "P"))))
; (display-theorems "P_Soundness")

)


(animate "P")


(begin
  
(sg "cP(℧(SUCC nat))=OP(℧nat)ø")
(assume "nat")
(ng)
(simp(pf"(℧nat= ø)=F"))
(use "Truth-Axiom")
(simp "BooleFalseRight")
(use "Truth-Axiom")
; Proof finished.
(save "ordPredOsn")
(display-theorems "ordPredOsn")

)

(deanimate "S")


(begin

(display "
   ( α=cP(α) ∧ β≺α )  →  cS(β) ≺α
")

(sg "(ord=cP ord ∧ ord0≺ord) → (cS(ord0) ≺ ord)")
(assume "ord" "ord0")
(ass "h")
(booleimp "(ord= ø ∨ ord≼ord0 ∨ cS(ord0) ≺ ord)")
(simp(pf"ord= ø -> F"))
(simp-with "h" 'right)
(use "Truth-Axiom")
(assume "=0")
(booleimp "ord0≺ord")
(simp "=0")
(use "Truth-Axiom")
(use-with "h" 'right)
(booleimp "ord=cP ord")
(use-with "P_Soundness" (pt"ord") (pt"ord0") 'left)
(use-with "h" 'left)
; Proof finished.
(nrw "(ord=cP ord ∧ ord0≺ord) → (cS(ord0) ≺ ord)")
(nrw "ord=(Rec ord=>ord)ø([ord1,ord2,ord3,ord4][if (ord1= ø ∧ord2= ø) ø (OP ord1 ord4)]) ord∧ ord0≺ord
      → cS ord0≺ord")
(nrw "ord=cP ord∧ord0≺ord→
      (Rec ord=>ord)①([ord1,ord2,ord3]OP ord1)ord0≺ord")
(nrw "ord= (Rec ord=>ord)ø
           ([ord1,ord2,ord3,ord4][if (ord1= ø ∧ord2= ø) ø (OP ord1 ord4)]) ord∧ ord0≺ord→
           (Rec ord=>ord)①([ord1,ord2,ord3]OP ord1)ord0≺ord")

)


(deanimate "P")




(display "

Extraction of cExpCont  from

  ∃ξ.  [ α=ξ → (α = ø ∨ ¬(α=cPα) ∨ ω^α≼β) ]
        [ α≠ξ → ( ξ≺α  ∧ β≺ω^ξ ) ]

")

(begin

(sg "all ord2,ord1 ex ord .
   (  ord1=ord   → (ord1 = ø ∨ ¬(ord1=cP ord1) ∨ ω^ ord1≼ord2))
  ∧(¬(ord1=ord) → (ord≺ord1 ∧ ord2≺ ω^ ord))")
(ind)
	(cases)
		(ex-intro (pt "ø"))
		(use "Truth-Axiom")
    (assume "ord11" "ord12")
    (ex-intro (pt "ø"))
    (use "Truth-Axiom")
(assume "ord21" "ord22" "IH21" "IH22" "ord1")
(cd "ord1= ø ∨ ¬(ord1=cP ord1) ∨ ω^ord1≼OP ord21 ord22" "*")
    (ex-intro (pt "ord1"))
    (use "Truth-Axiom")
(assume "#")
(ca "¬(ord1= ø ∨ ¬(ord1=cP ord1)∨ ω^ord1≼OP ord21 ord22)" "@")
(drop "#")
(ng "@" #t)
(inst-with-to "IH22" (pt "ord1")  "ih")
(drop "IH21" "IH22")
(by-assume-with "ih" "ord" "h")
(ca  "ord≺ord1∧ord22≺ ω^ord" "+")
(drop "h")
(cd "ord21≺ord" "21<")
    (drop "@")
    (ex-intro(pt"ord"))
    (simp "21<")
    (simp(pf"(ord1=ord)->F"))
    (use "+")
    (assume "gl")
    (booleimp "ord≺ord1")
    (simp "gl")
    (use "Truth-Axiom")
    (use-with "+" 'left)
(assume "21≮")
(ex-intro(pt"cS ord21"))
(ng #t)
(cas "cS ord21≺ord1" "$")
(simp (pf"ord1=cS ord21 -> F"))
(ng #t)
(trans "ω^ord")
(simp-with "+" 'right)
(ng #t)
(simp "21≮")
(use "Truth-Axiom")
(assume "gl")
(booleimp "cS ord21≺ord1")
(simp "gl")
(use "Truth-Axiom")
(use "$")
(booleimp "ord1=cP ord1∧ord21≺ord1")
(use "Truth-Axiom")
(simp-with "@" 'left 'right)
(booleimp "OP ord21 ord22≺ ω^ord1")
(use "Truth-Axiom")
(use-with "@"  'right)
(booleimp "(ord1=ord→ord1= ø ∨ ¬(ord1=cP ord1)∨ ω^ord1≼ord22)∧(ord1=ord∨ord≺ord1∧ord22≺ ω^ord)")
(simp-with "@" 'left 'right)
(simp-with "@" 'left 'left)
(ng #t)
(cd "ord1=ord" "gl")
	(ng #t)
	(simp "<-" "gl")
	(ng #t)
	(booleimp "OP ord21 ord22≺ ω^ord1")
	(use "Truth-Axiom")
	(use-with "@" 'right)
(auto)
(simp "#")
(use "Truth-Axiom")
; Proof finished.
(save "ExpCont")
(display-theorems "ExpCont")

(animate "S")
(animate "P")
(newline)
(test-extracted-binary "ExpCont")
(newline)
(deanimate "P")
(deanimate "S")
)



(begin

(add-program-constant
 "ordnexp"
 (mk-arrow (py "ord") (py "nat") (py "ord"))
 1 'const 2)

; Computation Rules

(acr "ordnexp ord 0"              "ø")
(acr "ordnexp ord (SUCC nat)"     "OP ord (ordnexp ord nat)")

(set! OLD-COMMENT-FLAG COMMENT-FLAG)
(set! COMMENT-FLAG #t)

(display-program-constants "ordnexp")
(newline)
(display "ordnexp (α,n) :≡ ω^α * n")
(newline)

(set! COMMENT-FLAG OLD-COMMENT-FLAG)

)


(display "

Extraction of cOmegaTimesCont  from

  ∀β ∀α ∃n.  [ ω^(Sα) ≼ β →   n = 0]
            ∧ [ β ≺ ω^(Sα) →  β ≺ w^α *n  ]

")


(begin

(sg "all ord2  ex nat .
   (ω^(cS ord1)≼ord2  → nat=0)
  ∧(ord2 ≺ ω^(cS ord1) → ord2 ≺ ordnexp ord1 nat)")
(assume "ord1")
(ind)
	(ex-intro (pt "1"))
	(use "Truth-Axiom")
(assume "ord21" "ord22" "IH21" "IH22")
(drop "IH21")
(cd "OP ord21 ord22 ≺ ω^ (cS ord1)" "kleiner")
	(ng)
	(ca "(ord21≼ord1)∧(ord22≺OP(cS ord1)ø)" "kl")
	(drop "kleiner")
	(by-assume-with "IH22" "nat" "ih")
	(ex-intro(pt "SUCC nat"))
	(ng)
	(simp(pf"(ord1≺ord21)=F"))
	(cas "ord22≺ordnexp ord1 nat" "+")
	(simp(pf"ord22≺OP ord1(ordnexp ord1 nat)"))
	(use "Truth-Axiom")
	(booleimp "ord22≺ordnexp ord1 nat")
	(use "Truth-Axiom")
	(use "+")
	(booleimp "ord22≺OP(cS ord1)ø")
	(use-with "ih" 'right)
	(use-with "kl" 'right)
	(simp "BooleFalseRight")
	(use-with "kl" 'left)
	(simp "<-" "booleIfAnd")
	(use "kleiner")
(assume "nkl")
(ex-intro(pt"0"))
(use "Truth-Axiom")
; Proof finished.
(save "OmegaTimesCont")
(display-theorems "OmegaTimesCont")

(test-extracted-binary "OmegaTimesCont")

)





(display "

End of hao_suc.scm
")



; EOF