;;; MINLOG: hao_relations.scm


(display"

Begin of hao_relations.scm

")



;; Predicate/Relation LESS   ≺


(begin

(add-program-constant
 "ordSMALLER"
 (mk-arrow (py "ord") (py "ord") (py "boole"))
 1 'const 2
)

; TOKENS

(define (smallerrel term1 term2)
  (mk-term-in-app-form
   (make-term-in-const-form (pconst-name-to-pconst "ordSMALLER")) term1 term2))

(add-token
 "≺"
 'rel-op
 (lambda (x y)(smallerrel x y)))

(add-token
 "≼"
 'rel-op
 (lambda (x y) (negboole  (smallerrel y x))))

(add-token
 "~"
 'rel-op
 (lambda (x y)
    (andboole
     (negboole (smallerrel y x))
     (negboole (smallerrel x y)))))




; DISPLAY

(define (smaller-boole? operator arguments)
  (and (term-in-const-form? operator)
       (string=? "ordSMALLER"
		 (const-to-name (term-in-const-form-to-const operator)))
       (= 2 (length arguments))))




(add-display
 (py "boole")
 (lambda (x)
   (if (term-in-app-form? x)
       (let* ((op (term-in-app-form-to-final-op x))
	      (args (term-in-app-form-to-args x)))
	 (if (smaller-boole? op args)
	     (let* ((constname (const-to-name (term-in-const-form-to-const op)))
		    (lhs (term-to-token-tree (car args)))
		    (rhs (term-to-token-tree (cadr args))))
	       (list 'add-op "≺" lhs rhs))
	     #f))
       #f)))


(add-display
 (py "boole")
 (lambda (x)
   (if (neg-boole? x)
       (let* ((op (term-in-app-form-to-final-op(neg-boole-to-kernel x)))
	      (args (term-in-app-form-to-args(neg-boole-to-kernel x))))
	 (if (smaller-boole? op args)
	     (let* ((constname (const-to-name (term-in-const-form-to-const op)))
		    (lhs (term-to-token-tree (cadr args)))
		    (rhs (term-to-token-tree (car args))))
	       (list 'rel-op "≼" lhs rhs))
	     #f))
       #f)))



(add-display
 (py "boole")
 (lambda (x)
   (if (and-boole? x)
       (let* ((lb (term-in-pair-form-to-left(and-boole-to-kernel x)))
	      (rb (term-in-pair-form-to-right(and-boole-to-kernel x))))
	 (if (and (neg-boole? lb) (neg-boole? rb))
	     (let* ((lop (term-in-app-form-to-final-op(neg-boole-to-kernel lb)))
		    (largs (term-in-app-form-to-args(neg-boole-to-kernel lb)))
		    (rop (term-in-app-form-to-final-op(neg-boole-to-kernel rb)))
		    (rargs (term-in-app-form-to-args(neg-boole-to-kernel rb))))
	       (if (and (smaller-boole? lop largs)
			(smaller-boole?  rop rargs)
			(equal? largs (reverse rargs)))
		   (list 'rel-op "~"
			 (term-to-token-tree (car rargs))
			 (term-to-token-tree (cadr rargs)))
		   #f))
	     #f))
       #f)))



; Computation Rules

(acr "ord ≺ ø"              "F")
(acr "ø ≺ (OP ord0 ord1)"   "T")
(acr "(OP ord0 ord1) ≺ (OP ord2 ord3)"
     "[if (ord0≺ord2) (ord1 ≺(OP ord2 ord3))
                      ([if (ord2≺ord0) ((OP ord0 ord1) ≺ ord3)
                                        (ord1 ≺ ord3)])]")


(define (smallersimp)
  (simp
   (pf "all ord0,ord1,ord2,ord3.
        (¬(ord0≺ord2∧ord1≺OP ord2 ord3)∧ ¬(ord0≼ord2∧ord1≺ord3)→OP ord0 ord1≺ord3)
        =(OP ord0 ord1≺OP ord2 ord3)")))




; ordMAX:    ord @ ord  ->  ord
(add-program-constant
 "ordMAX" (mk-arrow (make-alg "ord") (make-alg "ord") (make-alg "ord"))
 1 'const 2)

(acr "ordMAX ord1 ord2" "[if (ord1≺ord2) (ord2) (ord1)]")




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

(display-program-constants "ordSMALLER")
(newline)
(display "NOTA BENE:  α≼β :≡ ¬(β≺α)      α~β :≡ α≼β ∧ β≼α")
(newline)(newline)

(display-program-constants "ordMAX")

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

)



(display "

RW-rules for ordSMALLER ≺

")

(begin

; 0 ≠ α  ⇔  0 ≺ α
(sg "(ø ≺ ord) = ¬(ord = ø)")
(cases)
(auto)
; Proof finished.
(arw "ø ≺ ord"   "¬(ord = ø)")

; α≺1 -> α=0
(set-goal(pf"(ord0 ≺ ①) =(ord0 = ø)"))
(cases)
(auto)
; Proof finished.
(arw "ord0 ≺ ①"   "ord0 = ø")


; ≺ irreflexsive : α ≮ α
(sg "¬(ord ≺ ord)")
(ind)
     (search)
(assume "ord0" "ord1" "IH0")
(ng)
(simp (pf "(ord0≺ord0)=F"))
(search)
(simp "BooleFalseRight")
(search)
; Proof finished.
(nrw "¬(ord ≺ ord)")

; α ≺ ω  ⇔  a ≺ 1+α
(sg "(ord ≺ OP ø ord) = (ord ≺ ω)")
(ind)
  (search)
(assume "ord1" "ord2")
(ng)
(cds "ord1= ø" "1=0")
(auto)
; Proof finished.
(arw "ord ≺ OP ø ord"  "ord ≺ ω")


(sg "(OP ord1 ord2 ≺ OP ø (OP ord1 ord2)) = ((ord1 = ø) ∧ (ord2 ≺ ω))")
(cases)
(auto)
; Proof finished.
(arw "OP ord1 ord2 ≺ OP ø (OP ord1 ord2)"
     "(ord1 = ø) ∧ (ord2 ≺ ω)")


; α ≺ ω  ⇔  1+α ≺ 2+α
(sg "(OP ø ord ≺ OP ø (OP ø ord)) = (ord ≺ ω)")
(auto)
; Proof finished.
(arw "ord ≺ OP ø (OP ø ord)"   "ord ≺ ω")


; ¬(1+α ≺ α)
(sg "¬(OP ø ord ≺ ord)")
(ind)
      (search)
(assume "ord1" "ord2")
(ng)
(cds "ord1= ø" "1= ø")
(auto)
; Proof finished.
(nrw "¬(OP ø ord ≺ ord)")

; α<2 = α=ø ∨ α=1
(sg "(ord≺ ②) = (ord= ø ∨ ord= ①)")
(cases)
  (auto)
(assume "ord1" "ord2")
(ng)
(cd "ord1= ø" "1=0")
(ng)
(cd "ord2= ø" "2=0")
(auto)
; Proof finished.
(arw "ord≺ ②"  "ord= ø ∨ ord= ①")


(sg "(ord1 ≺OP ø (ω^ ord2)) = [if (ord2 = ø) (ord1≺ ②) (ord1 ≺(ω^ ord2))]")
(cases)
   (auto)
(assume "ord11" "ord12")
(ng)
(cds "ord11= ø" "11=0")
  (ng)
  (cases)
    (search)
  (search)
(assume "11≠0")
(ng)
(cases)
(auto)
; Proof finished.
(arw "ord2 ≺OP ø (ω^ ord1)"
     "[if (ord1 = ø) ([if (ord2= ø)(T)(ord1= ①)]) (ord2 ≺(ω^ ord1))]")



(sg "[if (¬(ord1= ø)) False (ord2≺OP ord1 ord2)] = (ord1 = ø ∧ ord2 ≺ ω)")
(cases)
(auto)
; Proof finished.
(arw "¬[if (¬(ord1= ø)) False (ord2≺OP ord1 ord2)]"
     "¬(ord1 = ø ∧ ord2 ≺ ω)")



; 1 < α  =  α≠0 & α≠1
(sg "(① ≺ord)=(¬(ord= ø)  ∧ ¬(ord= ①))")
(cases)
(auto)
(assume "ord1" "ord2")
(ng #t)
(cases(pt"ord1 = ø"))
(auto)
; Proof finished.
(add-rewrite-rule
 (pt"① ≺ord")
 (pt"¬(ord= ø)  ∧ ¬(ord= ①)"))


; ≺ antisymmetric :  ¬( α≺β ∧ β≺α )
(sg "¬(ord1≺ord2 ∧ ord2≺ord1)")
(ind)
   (search)
(assume "ord11" "ord12" "IH11" "IH12")
(ind)
    (search)
(assume "ord21" "ord22" "IH21" "IH22")
(ng #t)
(cd "ord11 ≺ ord21" "11<21")
(ng #t)
(simp (pf"(ord21≺ord11)=F"))
(use "IH12")
(simp "<-" (pf"(ord11≺ord21 ∧ ord21≺ord11) =F"))
(simp "11<21")
(auto)
(simp "BooleFalseRight")
(auto)
(assume "11≮21")
(ng #t)
(cases (pt"ord21≺ord11"))
(auto)
; Proof finished.
(nrw "¬(ord1≺ord2 ∧ ord2≺ord1)")


(sg "ord1≺ord2→(ord2≺ord1)=F")
(assume "ord1" "ord2")
(cd "ord1≺ord2" "1<2")
(ng)
(simp "BooleFalseRight")
(booleimp "ord1≺ord2")
(auto)
; Proof finished.
(nrw "ord1≺ord2→(ord2≺ord1)=F")

(set! OLD-COMMENT-FLAG COMMENT-FLAG)
(set! COMMENT-FLAG #t)
(newline)
(display "ord ≺ ord                 =  ")(pnt"ord≺ord")
(display "ord1≺ord2 ∧ ord2≺ord1    =  ")(pnt"ord1≺ord2 ∧ ord2≺ord1")
(display "ord1≼ord2 ∨ ord2≼ord1    =  ")(pnt"ord1≼ord2 ∨ ord2≼ord1")

(display"

RW rules's end

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

(display-program-constants "ordSMALLER")
)



(display "
≺ and ≼ are transitive.

Proof takes a while !

")
(time(begin
(sg "all ord0,ord1,ord2.
        ((ord0 ≼ ord1 ∧ ord1 ≺ ord2) → ord0 ≺ ord2)
     ∧ ((ord2 ≼ ord0 ∧ ord0 ≺ ord1) → ord2 ≺ ord1)
     ∧ ((ord1 ≼ ord2 ∧ ord2 ≺ ord0) → ord1 ≺ ord0)
     ∧ ((ord0 ≺ ord1 ∧ ord1 ≼ ord2) → ord0 ≺ ord2)
     ∧ ((ord2 ≺ ord0 ∧ ord0 ≼ ord1) → ord2 ≺ ord1)
     ∧ ((ord1 ≺ ord2 ∧ ord2 ≼ ord0) → ord1 ≺ ord0)")

(ind); on ord0

; ord0 = 0
(ind); on ord1
  (auto)
(assume "ord5" "ord6")
(strip 2)
(ind)
     (search)
(assume "ord7" "ord8")
(strip)
(use "Truth-Axiom")

; END of ord0 = ø

(assume "ord3" "ord4")
(strip 2)

(ind); on ord1
    (strip)
    (use "Truth-Axiom")
(assume "ord5" "ord6")
(strip 2)
(ind); on ord2
    (use "Truth-Axiom")
(assume "ord7" "ord8")
(strip)
(drop '3 5)
(cd "ord3≺ord5" "3<5")
(drop 4)
(ng #t)
(simp "3<5")
(cas "(ord5≺ord3)=F" "3≤5")
(ng #t)
(cd "ord3≺ord7" "3<7")
(simp (pf"(ord7≺ord3)=F"))
(ng #t)
(use-with 2 (pt"OP ord5 ord6") (pt"OP ord7 ord8"))
(drop '1 2 3 4 5 6)
(booleimp "ord3≺ord7")
(use "Truth-Axiom")
(use "3<7")
; ?_37: (ord3≺ord7 -> F) ->...
(assume "7≤3")
(ng #t)
(cas "ord7≺ord5" "7<5")
(simp(pf"(ord5≺ord7)=F"))
(ng #t)
(cd "ord7≺ord3" "7<3")
(drop '1 2)
(ng #t)
(simp(pf"(OP ord5 ord6≺ord4) = (OP ord5 ord6≺OP ord3 ord4)"))
(simp(pf"(ord4≺OP ord5 ord6) = (OP ord3 ord4≺OP ord5 ord6)"))
(use 6)
(drop 6)
(ng)
(simp "3<5")
(auto)
(drop '1 2 6)
(ng)
(simp "3≤5")
(simp "3<5")
(use "Truth-Axiom")
(drop '1 2 6)
(search)
(drop '1 2 6)
(booleimp "ord7≺ord5")
(use "Truth-Axiom")
(use "7<5")
(drop '2 '6)
(booleimp "(ord7≼ord3 ∧ ord3≺ord5)")
(use-with 1 (pt"ord5") (pt"ord7") 'left 'left 'left 'left 'right)
(drop 1)
(simp "7≤3")
(use "3<5")
(drop '1 2 6)
(booleimp "ord3≺ord5")
(use "Truth-Axiom")
(use "3<5")
; ?_45: (ord3≺ ord5 -> F) ->...
(assume "5≤3")
(ng #t)
(simp "5≤3")
(ng #t)
(cd "ord5≺ord3" "5<3")
(ng #t)
(cd "ord5≺ord7" "5<7")
(drop '1 '2 '6)
(simp (pf"(ord7≺ ord5)=F"))
(ng #t)
(use-with 4 (pt"OP ord7 ord8"))
(drop 4)
(booleimp "ord5≺ord7")
(use "Truth-Axiom")
(use "5<7")
; ?_117: (ord5≺ord7 -> F) ->...
(assume "7≤5")
(cas "ord7≺ord3" "7<3")
(simp (pf"(ord3≺ord7)=F"))
(ng #t)
(cd "ord7≺ ord5" "7<5")
(simp(pf"(ord6≺OP ord3 ord4) = (OP ord5 ord6≺OP ord3 ord4)"))
(simp(pf"(OP ord3 ord4≺ord6) = (OP ord3 ord4≺OP ord5 ord6)"))
(use 6)
(drop 6)
(ng #t)
(simp "5≤3")
(simp "5<3")
(auto)
(drop '1 '2 '4 '6)
(ng #t)
(simp "5≤3")
(simp "5<3")
(use "Truth-Axiom")
(search)
(drop '1 '2 '4 '6)
(booleimp "ord7≺ord3")
(use "Truth-Axiom")
(use "7<3")
(drop '2 '4 '6)
(booleimp "(ord7≼ord5 ∧ ord5≺ord3)")
(use-with 1 (pt"ord7") (pt"ord5") 'left 'left 'left 'right)
(drop 1)
(simp "7≤5")
(use "5<3")
; ?_85: (ord5≺ord3 -> F) ->...
(assume "3≤5")
(cd "ord5≺ord7" "5<7")
(simp (pf"(ord7≺ ord5)=F"))
(ng #t)
(cas "ord3≺ord7" "3<7")
(simp (pf"(ord7≺ord3)=F"))
(ng #t)
(use 2)
(drop '1 2 3 4 6)
(booleimp "ord3≺ord7")
(use "Truth-Axiom")
(use "3<7")
(drop '2 3 4 6)
(booleimp "(ord3≼ord5 ∧ ord5≺ord7)")
(use-with 1 (pt"ord5") (pt"ord7") 'left 'left 'left 'left 'left)
(drop 1)
(simp "3≤5")
(use "5<7")
(drop '1 2 3 4 6)
(booleimp "ord5≺ord7")
(use "Truth-Axiom")
(use "5<7")
; ?_146: (ord5≺ord7 -> F) ->...
(assume "7≤5")
(ng #t)
(cd "ord7≺ ord5" "7<5")
(cas "ord7≺ord3" "7<3")
(simp (pf"(ord3≺ord7)=F"))
(ng #t)
(drop '1 2 3 4 5)
(simp(pf"(ord6≺ord4)=(OP ord5 ord6≺OP ord3 ord4)"))
(simp(pf"(ord4≺ord6)=(OP ord3 ord4≺OP ord5 ord6)"))
(use 6)
(drop '1 '2 '3 '4 '5 '6)
(ng #t)
(simp "3≤5")
(simp "5≤3")
(use "Truth-Axiom")
(drop '1 '2 '3 '4 '5 '6)
(ng #t)
(simp "3≤5")
(simp "5≤3")
(use "Truth-Axiom")
(drop '1 '2 '3 '4 '5 '6)
(booleimp "ord7≺ord3")
(use "Truth-Axiom")
(use "7<3")
(drop '2 '3 '4 '5 '6)
(booleimp "(ord7≺ord5 ∧ ord5≼ord3)")
(use-with 1 (pt"ord7") (pt"ord5") 'right)
(drop 1)
(ng #t)
(simp "5≤3")
(use "7<5")
; ?_157: (ord7≺ ord5 -> F) ->...
(assume "5≤7")
(ng #t)
(simp(pf"(ord3≺ord7)=F"))
(simp(pf"(ord7≺ord3)=F"))
(ng #t)
(use 2)
(drop '2 3 4 5 6)
(simp "<-" (pf"(ord7≺ord3 ∧ ord3≼ord5 ∧ ¬(ord7≺ord5))=F"))
(drop 1)
(ng #t)
(simp "3≤5")
(simp "5≤7")
(use "Truth-Axiom")
(simp "BooleFalseRight")
(use-with 1 (pt"ord5") (pt"ord7") 'left 'right)
(drop '2 3 4 5 6)
(simp "<-" (pf"(ord5≼ord3 ∧ ord3≺ord7 ∧ ¬(ord5≺ord7))=F"))
(drop 1)
(ng #t)
(simp "5≤3")
(simp "7≤5")
(use "Truth-Axiom")
(simp "BooleFalseRight")
(use-with 1 (pt"ord7") (pt"ord5") 'left  'left  'left  'left 'right)
; Proof finished.
(nrw "(ord0≼ord1 ∧ ord1≺ord2) → ord0 ≺ ord2")
(nrw "(ord0≺ord1 ∧ ord1≼ord2) → ord0 ≺ ord2")


; ≺ transitive (α ≺ β  ∧  β ≺ γ)  →  α ≺ γ

(sg "(ord1≺ord2 ∧ ord2≺ord3) → (ord1≺ord3)")
(assume "ord1" "ord2" "ord3")
(cases (pt"ord1≺ord3"))
  (search)
(assume"3≤1")
(ng)
(cases (pt"ord2≺ord3"))
(assume "2<3")
(ng)
(cd " ord1≺ord2" "1<2")
(ng #t)
(simp "<-" (pf"(ord2≺ord3 ∧ ord3≼ord1 ∧ ord1≼ord2)=F"))
(simp "2<3")
(simp "3≤1")
(booleimp "ord1≺ord2")
(auto)
; Proof finished.
(save "ordSmallerTrans")
(display-theorems "ordSmallerTrans")
(nrw "(ord1≺ord2 ∧ ord2≺ord3) → (ord1≺ord3)")


(sg "¬(ord1≼ord2∧ord2≺ord3∧ord3≺ord1)")
(assume "ord2" "ord1" "ord3")
(simp(pf"((ord1≼ord2 ∧ ord2≺ord3) → ord1≼ord3)=((ord2≺ord3 ∧ ord3≺ord1) → ord2≺ord1)"))
(use "Truth-Axiom")
(cases(pt"ord2≺ord1"))
(auto)
;  Proof finished.
(nrw "¬(ord1≼ord2∧ord2≺ord3∧ord3≺ord1)")


(sg "¬(ord1≺ord2∧ord2≼ord3∧ord3≺ord1)")
(assume "ord1" "ord2" "ord3")
(simp(pf"((ord1≺ord2 ∧ ord2≼ord3) → ord1≼ord3)=((ord3≺ord1 ∧ ord1≺ord2) → ord3≺ord2)"))
(use "Truth-Axiom")
(cases(pt"ord3≺ord1"))
(auto)
;  Proof finished.
(nrw "¬(ord1≺ord2∧ord2≼ord3∧ord3≺ord1)")


; ≼ transitive (α ≼ β  ∧  β ≼ γ)  →  α ≼ γ

(sg "¬(ord1≼ord2∧ord2≼ord3∧ord3≺ord1)")
(assume "ord2" "ord1" "ord3")
(simp(pf"((ord1 ≼ ord2 ∧ ord2≼ord3) → (ord1≼ord3)) = ((ord3≺ord1 ∧ ord1≼ord2) → ord3≺ord2)"))
(use "Truth-Axiom")
(cases(pt"ord3≺ord1"))
(auto)
; Proof finished.
(save "ordSmallereqTrans")
(display-theorems "ordSmallereqTrans")
(nrw "¬(ord1≼ord2∧ord2≼ord3∧ord3≺ord1)")


(sg "¬(¬[if (ord21≺ord11) (ord22≺OP ord11 ord12) [if (ord11≺ord21) (OP ord21 ord22≺ord12) (ord22≺ord12)]]
       ∧OP ord21 ord22≼ord3∧ord3≺OP ord11 ord12)")
(cut
 (pf"all ord21,ord11,ord22,ord12,ord3
     OP ord11 ord12≼OP ord21 ord22∧OP ord21 ord22≼ord3→OP ord11 ord12≼ord3"))
(search)
(strip)
(use-with
 (pf "all ord1,ord2,ord3. (ord1≼ord2∧ord2≼ord3)→ord1≼ord3")
 (pt "OP ord11 ord12") (pt "OP ord21 ord22") (pt "ord3"))
(search)
; Proof finished.
(nrw "¬(¬[if (ord21≺ord11) (ord22≺OP ord11 ord12) [if (ord11≺ord21) (OP ord21 ord22≺ord12) (ord22≺ord12)]]
       ∧OP ord21 ord22≼ord3∧ord3≺OP ord11 ord12)")




;;;;;;;; ordSMALLER is partial order ;;;;;;;


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

(display "≺ is strict partial order:

")
(display "ord≺ord                                =  ")(pnt"ord≺ord")
(display "ord1≺ord2 ∧ ord2≺ord1                 =  ")(pnt"ord1≺ord2 ∧ ord2≺ord1")
(display "(ord1≺ord2 ∧ ord2≺ord3) → ord1≺ord3  =  ")(pnt"(ord1≺ord2 ∧ ord2≺ord3) → (ord1≺ord3)")

(display "
≼ is reflexsiv total order:

")
(display "ord≼ord                                =  ")(pnt"ord≼ord")
(display "(ord1≼ord2 ∧ ord2≼ord3) → ord1≼ord3  =  ")(pnt"(ord1≼ord2 ∧ ord2≼ord3) → (ord1≼ord3)")
(display "ord1≼ord2 ∨ ord2≼ord1                 =  ")(pnt"ord1≼ord2 ∨ ord2≼ord1")
(newline)
(set! COMMENT-FLAG OLD-COMMENT-FLAG)
))





(display"

Some more RW-rules

")

(begin

(sg "ord≺OP ord1 ø →ord≺OP ord1 ord2")
(assume "ord" "ord1" "ord2")
(cut
 (pf "(ord≺OP ord1 ø ∧OP ord1 ø  ≼ OP ord1 ord2)→ord≺OP ord1 ord2"))
(search)
(use (pf"all ord1,ord2,ord3.(ord1 ≺ ord2 ∧ ord2 ≼ ord3) → ord1 ≺ ord3"))
(search)
; Proof finished.
(nrw "ord12≺OP(OP ord11 ord12)ø →ord12≺OP(OP ord11 ord12)(OP ord21 ord22)")


(sg "¬(ord≼OP ord1 ord∧ord≼ord2∧OP ord1 ord2 ≺ord)")
(assume "ord1" "ord" "ord2")
(cut (pf "ord≼OP ord1 ord∧OP ord1 ord≼OP ord1 ord2 →ord≼OP ord1 ord2"))
(search)
(use (pf"all ord1,ord2,ord3.(ord1 ≼ ord2 ∧ ord2 ≼ ord3) → ord1 ≼ ord3"))
(search)
; Proof finished.
(nrw "¬(ord≼OP ord1 ord∧ord≼ord2∧OP ord1 ord2 ≺ord)")



(sg "all ord1,ord2.ord1 ≺OP ord1 ord2 ∧ ord1≼OP ord2 ord1")
(ind); ord1
    (search)
(assume "ord11" "ord12" "IH11" "IH12")
(ca "all ord2.(OP ord2 ord12≺ord12)=F" "IH12r")
(ca "all ord2.ord12≺OP ord12 ord2" "IH12l")
(ca "ord12≺OP (OP ord11 ord12) ø" "12<(11 12)0")
(drop "IH12")
(ng #t)
(cas "ord11≺OP ord11 ord12" "11≺11 12")
(ng #t)
(ind); ord2
    (ng #t)
    (simp "12<(11 12)0")
    (cds "ord11= ø" "11=0")
    (search)
    (search)
(assume "ord21" "ord22" "IH21" "IH22")
(drop  "IH21" "IH22")
(cd "OP ord21 ord22≺ord11" "(21 22)<11")
(ng #t)
(trans "OP(OP ord11 ord12)ø")
(search)
(assume "11≤21 22")
(ng #t)
(simp "IH12r")
(simp(pf"(OP(OP ord21 ord22)(OP ord11 ord12)≺ord12)=F"))
(ng #t)
(trans "OP(OP ord11 ord12)ø")
(search)
(booleimp "ord12 ≼ OP(OP ord21 ord22)(OP ord11 ord12)")
(use "Truth-Axiom")
(trans "OP (OP ord21 ord22) ord12")
(ng #t)
(simp "IH12r")
(simp "IH12r")
(use "Truth-Axiom")
(use-with "IH11" (pt"ord12") 'left)
(cases(pt "ord12≺OP(OP ord11 ord12)ø"))
  (search)
(assume "(11 12)0≤12")
(simp "<-" (pf"((ord12≺OP ord12 ø ∧ OP ord12 ø ≼ OP(OP ord11 ord12)ø) ∧ OP(OP ord11 ord12)ø ≼ ord12)=F"))
(simp "(11 12)0≤12")
(simp "IH12l")
(ng #t)
(simp "IH12r")
(use "Truth-Axiom")
(simp(pf"all ord1,ord2,ord3.((ord1≺ord2 ∧ ord2≼ord3)∧ ord3≼ord1)=F"))
(auto)
(ng #t)
(assume "ord2")
(use-with "IH12" (pt"ord2") 'left)
(assume "ord2")
(booleimp "ord12≼OP ord2 ord12")
(use "Truth-Axiom")
(use-with "IH12" (pt"ord2") 'right)
; Proof finished.
(trw "ord1 ≺OP ord1 ord2")
(nrw "ord1≼OP ord2 ord1")


(sg "(ω⋆ord ≺ ω)=(ord= ø)")
(cases)
(auto)
; Proof finished.
(arw "ω⋆ord ≺ ω" "ord= ø")


;  α ≼ ω^α+β
(sg "ord1≼OP ord1 ord2")
(assume "ord1" "ord2")
(booleimp "ord1≺OP ord1 ord2")
(use (pf"all ord1,ord2.ord1≺ord2→ord1≼ord2"))
(auto)
; Proof finished.
(nrw "ord1≼OP ord1 ord2")




(sg "¬(ord≼ord1∧OP ord1 ord2≺ord)")
(assume "ord1" "ord" "ord2")
(simp(pf "(¬(ord≼ord1∧OP ord1 ord2≺ord))=(¬(ord≼ord1∧ord1≼OP ord1 ord2∧OP ord1 ord2≺ord))"))
(use "ordSmallereqTrans")
(use "Truth-Axiom")
; Proof finished.
(nrw "¬(ord≼ord1∧OP ord1 ord2≺ord)")


(sg "¬(ord≼ord2∧OP ord1 ord2≺ord)")
(assume "ord2" "ord" "ord1")
(use-with (pf"all ord1,ord2,ord3.(ord1≼ord2∧ord2≼ord3)→ord1≼ord3")
	  (pt"ord") (pt"ord2") (pt"OP ord1 ord2"))
(search)
; Proof finished.
(nrw "¬(ord≼ord2∧OP ord1 ord2≺ord)")



; β≤α → ω^β+γ ≤ ω^α+γ
(sg"(ord2 ≼ ord1) → (OP ord2 ord3 ≼ OP ord1 ord3)")
(assume "ord2" "ord1" "ord3")
(ng #t)
(cases(pt"ord2≺ord1"))
(auto)
; Proof finished.
(nrw "(ord2 ≼ ord1) → (OP ord2 ord3 ≼ OP ord1 ord3)")



(sg "ord1≺ ω ∧[if (¬(ord2= ø)) True (¬(ω⋆ord3= ø))]→ord1≺OP(OPøord2)(ω⋆ord3)")
(assume "ord1" "ord2" "ord3")
(simp (pf "[if (¬(ord2= ø)) True (¬(ω⋆ord3= ø))]=(ω ≺ OP(OPøord2)(ω⋆ord3))"))
(use (pf"all ord1,ord2,ord3.ord1≺ord2∧ord2≺ord3→ord1≺ord3"))
(auto)
; Proof finished.
(nrw "ord1≺ ω ∧[if (¬(ord2= ø)) True (¬(ω⋆ord3= ø))]→ord1≺OP(OPøord2)(ω⋆ord3)")


; 0 ≠ α ≺ ω  → α ≠  ω * β
;(sg "(¬(ord2= ø) ∧ ord2≺ ω)→ ¬(ord2~ ω⋆ord)")
(sg "¬(ord2= ø)∧ord2≺ ω ∧ord2≼ ω⋆ord1→ord2≺ ω⋆ord1")
(cases)
  (search)
(assume "ord21" "ord22")
(cases)
  (search)
(assume "ord11" "ord12")
(ng #t)
(cds "ord21 = ø" "21=0")
(ng #t)
(cd "ord22≺ ω" "22<w")
(ng #t)
(simp (pf"ord22≺OP(OPøord11)(ω⋆ord12)"))
(use "Truth-Axiom")
(booleimp "(ord22 ≺ ω) ∧ (ω ≼ OP(OPøord11)(ω⋆ord12))")
(use (pf"all ord1,ord2,ord3.ord1≺ord2∧ord2≼ord3→ord1≺ord3"))
(auto)
; Proof finished.
(nrw "¬(ord2= ø)∧ord2≺ ω ∧ord2≼ ω⋆ord1→ord2≺ ω⋆ord1")


(sg "ord3≼OP ord1(OP ord2 ord3)")
(assume "ord1" "ord2" "ord3")
(booleimp "ord3≼OP ord2 ord3∧OP ord2 ord3≼OP ord1(OP ord2 ord3)")
(use (pf"all ord1,ord2,ord3.(ord1≼ord2∧ord2≼ord3)→ord1≼ord3"))
(search)
(booleimp "OP ord2 ord3≼OP ord1(OP ord2 ord3)")
(simp (pf"ord3≼OP ord2 ord3"))
(auto)
(use (pf"all ord1,ord2 ord2≼OP ord1 ord2"))
(auto)
; Proof finished.
(nrw "ord3≼OP ord1(OP ord2 ord3)")



(sg "ord≺OP ord1 ord2→ord≺OP ord1(OP ord3 ord2)")
(assume "ord" "ord1" "ord2" "ord3")
(cd "ord≺OP ord1 ord2" "<")
(ng)
(booleimp "ord≺OP ord1 ord2 ∧ OP ord1 ord2≼OP ord1(OP ord3 ord2)")
(use (pf"all ord1,ord2,ord3. ord1≺ord2∧ord2≼ord3→ord1≺ord3"))
(auto)
; Proof finished.
(nrw "ord≺OP ord1 ord2→ord≺OP ord1(OP ord3 ord2)")



(sg "all ord1,ord2,ord .
    [if (ord1≺ord) (ord2≺OP ord(OP ord1 ord2))[if (ord≺ord1) False (ord2≺OP ord1 ord2)]]
    → ord2≺OP ord(OP ord1 ord2)")
; (sg "OP ord1 ord2≺OP ord(OP ord1 ord2)→ord2≺OP ord(OP ord1 ord2)")
(assume "ord1" "ord2" "ord")
(cd "[if (ord1≺ord) (ord2≺OP ord(OP ord1 ord2)) [if (ord≺ord1) False (ord2≺OP ord1 ord2)]]" "<")
(ng #t)
(booleimp "ord2≼OP ord1 ord2 ∧ OP ord1 ord2≺OP ord(OP ord1 ord2)")
(use-with (pf"all ord1,ord2,ord3. ord1≼ord2∧ord2≺ord3→ord1≺ord3")
	  (pt "ord2") (pt "OP ord1 ord2") (pt "OP ord(OP ord1 ord2)"))
(auto)
; Proof finished.
(nrw "[if (ord1≺ord) (ord2≺OP ord(OP ord1 ord2))[if (ord≺ord1) False (ord2≺OP ord1 ord2)]]
       → ord2≺OP ord(OP ord1 ord2)")

(pnt "OP ord1 ord2≺OP ord(OP ord1 ord2)→ord2≺OP ord(OP ord1 ord2)")
; True

(sg "ord1≺OP ord2 ø ∧ ord2≺ord3→ord1≺OP ord3 ø")
(assume "ord1" "ord2" "ord3")
(use-with "ordSmallerTrans"
		  (pt"ord1") (pt"OP ord2ø") (pt"OP ord3ø"))
; Proof finished.
(nrw "ord1≺OP ord2 ø ∧ ord2≺ord3→ord1≺OP ord3 ø")


(sg "ord1≺ord2 → ord1≺OP ord ord2")
(assume "ord1" "ord2" "ord")
(ass "kl")
(booleimp "ord1≺ord2 ∧ ord2≼OP ord ord2")
(use(pf"all ord1,ord2,ord3.(ord1≺ord2 ∧ ord2≼ord3)→ord1≺ord3"))
(auto)
; Proof finished.
(nrw "ord1≺ord2 → ord1≺OP ord ord2")



(display"

End of ≺'s additional RW-rules

")


)






; already normalising when ~ defined by ≼ and ≽

(begin
(pnt  "ord ~ ø")
; ord= ø
(pnt  "ø ~ ord")
; ord= ø
(pnt "ord ~ OP ø ord")
; ω ≼ord
(pnt " OP ø ord ~ ord")
; ω ≼ord
(pnt "ord1 ~ OP ord1 ord2") 
; False
(pnt "OP ord1 ord2 ~ ord1")
; False
(pnt "ord2 ~ OP ord1 ord2") 
; OP ord1 ord2≼ord2
(pnt "OP ord1 ord2 ~ ord2")
; OP ord1 ord2≼ord2
)


(begin

(sg "(ord1 ~ ord2) = (ord2 ~ ord1)")
(assume "ord1" "ord2")
(simp "ANDcomm")
(use "Truth-Axiom")
; Proof finished.
(save"ICsym")
(display-theorems"ICsym")


(sg "(ord1 ~ ord2 ∧ ord2≼ord3∧ord3≼ord2) → ord1 ~ ord3")
(assume "ord2" "ord1" "ord3")
(cd "ord1 ~ ord2 ∧ ord2≼ord3∧ord3≼ord2" "(*)")
(simp (pf"ord1≼ord3"))
(simp (pf"ord3≼ord1"))
(use "Truth-Axiom")
(trans "ord2")
(simp-with "(*)" 'right)
(use-with "(*)"  'left 'left 'right)
(trans "ord2")
(simp-with "(*)" 'left 'left 'left)
(simp-with "(*)" 'left 'right)
(auto)
; Proof finished.
(nrw "(ord1 ~ ord2 ∧ ord2≼ord3∧ord3≼ord2) → ord1 ~ ord3")


(sg "((ord1≺ord2∨ord2≺ord1)∧ord1≼ord2)→ord1≺ord2")
(assume "ord1" "ord2")
(cd "ord1≺ord2" "1<2")
(auto)
; Proof finished.
(nrw "((ord1≺ord2∨ord2≺ord1)∧ord1≼ord2)→ord1≺ord2")



(define (ordeqtrans termstring)
  (let* ((err "ordeqtrans: Goal formula must be an atom of the form α ~ β  !!!")
	 (gf (goal-to-formula(current-goal))))
    (if (atom-form? gf)
	(let ((ggf (atom-form-to-kernel gf)))
	  (if (and-boole? ggf)
	      (let* ((kggf (and-boole-to-kernel ggf))
		     (lb   (term-in-pair-form-to-left  kggf))
		     (rb   (term-in-pair-form-to-right kggf)))
		(if (and (neg-boole? lb) (neg-boole? rb))
		    (let* ((klb (neg-boole-to-kernel lb))
			   (krb (neg-boole-to-kernel rb))
			   (lop   (term-in-app-form-to-final-op klb))
			   (largs (term-in-app-form-to-args     klb))
			   (rop   (term-in-app-form-to-final-op krb))
			   (rargs (term-in-app-form-to-args     krb)))
		      (if (and (smaller-boole?  lop largs)
			       (smaller-boole?  rop rargs)
			       (equal? largs (reverse rargs)))
			  (let* ((term (pt termstring))
				 (lhs (car  rargs))
				 (rhs (cadr rargs)))
			    (set! OLD-COMMENT-FLAG COMMENT-FLAG)
			    (set! COMMENT-FLAG #f)
			    (use "BooleImp"
				 (andboole
				  (andboole
				   (negboole (smallerrel term lhs))
				   (negboole (smallerrel lhs term)))
				  (andboole
				   (negboole (smallerrel rhs term))
				   (negboole (smallerrel term rhs)))))
			    (use-with (pf "all ord1,ord2,ord3.(ord1~ord2 ∧ ord2~ord3) → ord1~ord3")
				      lhs term rhs)
			    (set! COMMENT-FLAG OLD-COMMENT-FLAG)
			    (search))
			  (myerror err)))
		    (myerror err)))
	      (myerror err)))
	(myerror err))))




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

(display"

Equality ~ is an equivalence relation:

1) Reflexsive:          ord ~ ord   :  ")
(pnt "ord ~ ord")

(display"

2) Symmetric: ")
(display-theorems"ICsym")
(display"

3) Transitive:          (ord1 ~ ord2 ∧ ord2 ~ ord3) → ord1 ~ ord3    :  ")
(pnt"(ord1 ~ ord2 ∧ ord2 ~ ord3) → ord1 ~ ord3")

(display"
And ≺ is a linear order:

ord1~ord2 ∨ ord2≼ord1 ∨ ord1≼ord2     : ")
(pnt"ord1~ord2 ∨ ord2≼ord1 ∨ ord1≼ord2")

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

)


(begin

(sg "(¬(ord1= ø) ∧ ord3≺OP ø (OP ord1 ord2)) → ord3≺OP ord1 ord2")
(cases)
   (auto)
(assume "ord11" "ord12")
(ng)
(cases)
   (auto)
(assume "ord31" "ord32" "ord2")
(ng)
(cds "ord31= ø" "31=0")
(auto)
; Proof finished.
(nrw "(¬(ord1= ø) ∧ ord3≺OP ø (OP ord1 ord2)) → ord3≺OP ord1 ord2")




(display"
α~β → (γ≺α = γ≺β)     α~β → (α≺γ = β≺γ)

α~β → (γ~α = γ~β)

")

(sg "ord1~ord2 → ((ord3 ≺ ord1) = (ord3 ≺ ord2))")
(assume "ord2" "ord1" "ord3")
(cd "ord1~ord2" "1=2")
(cd "ord3≺ord1" "3<1")
(booleimp "ord3≺ord2")
(cases (pt"ord3≺ord2"))
(auto)
(booleimp "ord3≺ord1 ∧ ord1≼ord2")
(use "Truth-Axiom")
(simp-with "1=2" 'left)
(use "3<1")
(assume "3≮1")
(booleimp "ord2≼ord3")
(cases (pt"ord3≺ord2"))
(auto)
(trans "ord1")
(simp "3≮1")
(use-with "1=2" 'right)
(auto)
; Proof finished.
(nrw "ord1~ord2 → ((ord3 ≺ ord1) = (ord3 ≺ ord2))")


(sg "ord1~ord2 → ((ord1 ≺ ord3) = (ord2≺ ord3))")
(assume "ord2" "ord1" "ord3")
(cd "ord1~ord2" "1=2")
(cd "ord1≺ord3" "1<3")
(booleimp "ord2≺ord3")
(cases (pt"ord2≺ord3"))
(auto)
(booleimp "ord2≼ord1 ∧ ord1≺ord3")
(use "Truth-Axiom")
(simp-with "1=2" 'right)
(use "1<3")
(assume "1≮3")
(booleimp "ord3≼ord2")
(cases (pt"ord2≺ord3"))
(auto)
(trans "ord1")
(simp "1≮3")
(use-with "1=2" 'left)
(auto)
; Proof finished.
(nrw "ord1~ord2 → ((ord1 ≺ ord3) = (ord2≺ ord3))")


(sg "(ord1 ~ ord2)→ ( (ord1 ~ ord3) = (ord2 ~ ord3)) ")
(assume "ord2" "ord1" "ord3")
(cd "ord1~ord2" "1=2")
(ng #t)
(simp (pf"(ord1≺ord3)=(ord2≺ord3)"))
(simp (pf"(ord3≺ord1)=(ord3≺ord2)"))
(use "Truth-Axiom")
(booleimp "ord1~ord2")
(auto)
(booleimp "ord1~ord2")
(auto)
; Proof finished.
(nrw "(ord1 ~ ord2)→ ( (ord1 ~ ord3) = (ord2 ~ ord3)) ")

)


(display "
ordPersistency:

α≺β →  [ ( ∀η≺β F^η  →  ∀η≺α F^η ) & ( ∃η≺α F^η  →  ∃η≺β F^η ) ]

")

(begin

(sg "ord1≺ord2 ->
      ((all ord. ord≺ord2 -> (Pvar ord)^ ord) -> (all ord. ord≺ord1 -> (Pvar ord)^ ord))
    & ((ex  ord. ord≺ord1 &  (Pvar ord)^ ord) -> (ex  ord. ord≺ord2 &  (Pvar ord)^ ord))")

(assume "ord1" "ord2" "1<2")
(split)
    (assume "hyp" "ord" "<")
    (use "hyp")
    (trans "ord1")
    (simp "1<2")
    (use "<")
(assume "hyp")
(by-assume-with "hyp" "ord" "(*)")
(ex-intro(pt"ord"))
(split)
    (trans "ord1")
    (simp "1<2")
    (use "(*)")
(use "(*)")
; Proof finished.
(save "ordPersistency")
(display-theorems "ordPersistency")
)


(display"
Extraction of minusexp:

ω^α ≼ β -> ∃ξ (β ~ OP α ξ)

cminusexp(α,β)  ~   α - ω^β

")

(begin

(sg "(ord1 ≺ OP ord2 ø) | (ex ord. ord1 ~ OP ord2 ord)")
(ind) ; 1
  (assume "ord2")
  (ng)
  (ex-intro (pt "F"))
  (split)
  (search)
  (assume "F")
  (ex-intro (pt "ø"))
  (use "F")
(assume "ord11" "ord12" "IH11" "IH12" "ord2")
(drop "IH11")
(ng)
(cd "ord11 ≺ ord2" "11<2")
(simp (pf "(ord2 ≺ ord11)=F"))
(ng)
(inst-with-to "IH12" (pt "ord2")  "IH12_2")
(by-assume-with  "IH12_2" "boole1"  "IH12_2p")
(ex-intro (pt"boole1"))
(ng)
(split)
(use  "IH12_2p" )
(ng)
(assume "b1")
(ex-elim (pf "ex ord.¬(OP ord2 ord≺ord12) ∧ ¬(ord12≺OP ord2 ord)"))
(use "IH12_2p")
(use "b1")
(assume "ord" "IH12_2ord")
(ex-intro (pt"ord"))
(search)
(simp "<-" (pf"(ord2≺ord11 ∧ ord11≺ord2)=F"))
(simp "11<2")
(search)
(use "Truth-Axiom")
(assume "2≤11")
(ex-intro (pt"T"))
(ng)
(split)
(search)
(assume "T")
(cd "ord2 ≺ ord11" "2<11")
(ex-intro (pt "OP ord11 ord12"))
(ng)
(use "T")
(assume "2≮11")
(ex-intro (pt"ord12"))
(ng)
(use "T")
; Proof finished.
(save "minusexp")
(display-theorems "minusexp")

(test-extracted-binary "minusexp")
)


(animate "minusexp")

(display "
We check some properties of cminusexp


left (cminusexp ord1 ord2)    =  ω^ord2 ≼ ord1

left(cminusexp α β)           =  α ~ OP β right(cminusexp α β)

α≺ω^β → right(cminusexp α β) =  ø
")

(begin

(sg "left (cminusexp ord1 ord2) = ((ω^ ord2)≼ord1)")
(ind) ; 1
  (ng)
  (cases)
  (auto)
(assume "ord11" "ord12"  "IH11" "IH12" "ord2")
(drop "IH11")
(ng)
(cd "ord11 ≺ ord2"  "11<2")
(auto)
; Proof finished.
(save "cminusexpTrue")
(display-theorems  "cminusexpTrue")


(sg "(¬left (cminusexp ord1 ord2)) = (ord1 ≺ (ω^ ord2))")
(assume "ord1" "ord2")
(simp "cminusexpTrue")
(use "Truth-Axiom")
; Proof finished.
(save "cminusexpFalse")
(display-theorems  "cminusexpFalse")


(sg "all ord1.left (cminusexp ord1 ord2) = (ord1 ~ OP ord2 (right (cminusexp ord1 ord2)))")
(assume "ord2")
(ind)
  (use "Truth-Axiom")
(assume "ord11" "ord12" "IH11" "IH12")
(drop "IH11")
(ng #t)
(cd "ord11≺ord2" "11<2")
(simp (pf "(ord2≺ord11)=F"))
(ng #t)
(simp "IH12")
(use "Truth-Axiom")
(booleimp "ord11≺ord2")
(auto)

(assume "2≤11")
(ng #t)
(cd "ord2≺ord11" "2<11")
(auto)
; Proof finished.
(save "minexp")
(display-theorems "minexp")



(sg "all ord1.(ord2 ≼ (ω^ ord1)) = (right(cminusexp ord2 ord1)= ø)")
(ind)
  (search)
(assume "ord21" "ord22" "IH21" "IH22" "ord1")
(ng #t)
(cd "ord21≺ord1" "21<1")
(simp(pf"(ord1≺ord21)=F"))
(ng #t)
(simp-with "<-" "IH22" (pt"ord1"))
(use "Truth-Axiom")
(booleimp "ord21≺ord1")
(use "Truth-Axiom")
(use "21<1")
(assume "1≤21")
(cd "ord1≺ord21" "1<21")
(auto)
; Proof finished.
(save "minusexpsmaller")
(display-theorems "minusexpsmaller")

(deanimate "minusexp")





(display"
α ≺ ω^β+[α-ω^β] = α<ω^β
")

(sg "all ord2,ord1.(ord2 ≺ OP ord1 (right (cminusexp ord2 ord1))) = (ord2 ≺ OP ord1 ø)")
(assume "ord2" "ord1")
(cd "ord2≺OP ord1 ø" "2< 1 0")
  (simp (pf"right(cminusexp ord2 ord1) = ø"))
  (simp "2< 1 0")
  (use "Truth-Axiom")
  (simp "<-" "minusexpsmaller")
  (ng)
  (booleimp "ord2≺OP ord1ø")
  (use "Truth-Axiom")
  (use  "2< 1 0")
(assume "2 ≮ 1 0")
(simp "BooleFalseRight")
(use-with (pf"ord2≼OP ord1(right(cminusexp ord2 ord1)) ∧ OP ord1 right(cminusexp ord2 ord1)≼ord2") 'right)
(ng #t)
(simp "<-" "minexp")
(simp "cminusexpTrue")
(ng)
(simp "2 ≮ 1 0")
(use "Truth-Axiom")
; Proof finished.
(arw "ord2 ≺ OP ord1 (right(cminusexp ord2 ord1))" "ord2 ≺ OP ord1 ø")
(arw "ord2 ≺ OP ord1 
              right((Rec ord=>ord=>boole@@ord)([ord3]False@ ø)
                    ([ord3,ord4,(ord=>boole@@ord)_5,(ord=>boole@@ord)_6,ord7]
                      [if (ord3≺ord7)
                        ((ord=>boole@@ord)_6 ord7)
                        (True@[if (ord7≺ord3) (OP ord3 ord4) ord4])])
                    ord2 ord1)"
     "ord2 ≺ OP ord1 ø")


(animate "minusexp")

(sg "right(cminusexp ord1 ord2) ≼ ord1")
(ind)
   (auto)
(assume "ord11" "ord12" "IH11" "IH12")
(drop "IH11")
(cases)
  (ng #t)
  (cd "ord11= ø" "11=0")
  (auto)
(assume "ord21" "ord22")
(cases(pt "OP ord11 ord12≺right(cminusexp(OP ord11 ord12)(OP ord21 ord22))"))
(ng #t)
(cd "ord11≺OP ord21 ord22" "11<21 22")
  (ng #t)
  (assume "11 12<12m21 22")
  (inst-with-to "IH12" (pt "OP ord21 ord22") "r12(21 22)≤12")
  (simp "<-"
	(pf"((ord12≼OP ord11 ord12 ∧ OP ord11 ord12≺right(cminusexp ord12(OP ord21 ord22)))
             ∧ ¬(ord12≺right(cminusexp ord12(OP ord21 ord22))))=F"))
  (simp-with  (pf "(ord12 ≺ right(cminusexp ord12 (OP ord21 ord22)))=F"))
  (ng #t)
  (simp "11 12<12m21 22")
  (use "Truth-Axiom")
  (simp "BooleFalseRight")
  (use "r12(21 22)≤12")
  (simp "BooleFalseRight")
  (use (pf "all ord1,ord2,ord3.(ord1≼ ord2  ∧ ord2≺ord3) → ord1≺ord3"))
  (search)
(assume "11≮21 22")
(ng #t)
(cd "OP ord21 ord22≺ord11" "21 22<11")
(auto)
; Proof finished.
(nrw "right(cminusexp ord1 ord2) ≼ ord1")
(nrw "right((Rec ord=>ord=>boole@@ord)([ord3]False@ ø)
            ([ord3,ord4,(ord=>boole@@ord)_5,(ord=>boole@@ord)_6,ord7]
              [if (ord3≺ord7)  ((ord=>boole@@ord)_6 ord7)
                (True@[if (ord7≺ord3) (OP ord3 ord4) ord4])])
            ord1 ord2)≼ ord1")

(deanimate "minusexp")

)


(display"
OPfunctional

(ord1~ord3 ∧ ord2~ord4) →  OP ord1 ord2 ~ OP ord3 ord4

")



(begin

(sg "ord1~ord3∧ord2≼ord4∧ord4≼ord2→ 
      ¬ [if (ord3≺ord1)(ord4≺OP ord1 ord2) [if (ord1≺ord3) (OP ord3 ord4≺ord2) (ord4≺ord2)]]
    ∧
      ¬ [if (ord1≺ord3)(ord2≺OP ord3 ord4) [if (ord3≺ord1) (OP ord1 ord2≺ord4) (ord2≺ord4)]]")
(assume "ord3" "ord1" "ord4" "ord2")
(ng)
(cd "ord3≺ord1" "3<1")
  (use "Truth-Axiom")
(assume "1≤3")
(ng)
(cd "ord1≺ord3" "1<3")
(auto)
; Proof finished.
(nrw "ord1~ord3∧ord2≼ord4∧ord4≼ord2→ 
      ¬ [if (ord3≺ord1)(ord4≺OP ord1 ord2) [if (ord1≺ord3) (OP ord3 ord4≺ord2) (ord4≺ord2)]]
    ∧
      ¬ [if (ord1≺ord3)(ord2≺OP ord3 ord4) [if (ord3≺ord1) (OP ord1 ord2≺ord4) (ord2≺ord4)]]")



(sg "ord11~ord21∧OP ord12 ord13≼ord22∧ord22≼OP ord12 ord13→ ¬[if (ord21≺ord11) (ord22≺OP ord11(OP ord12 ord13)) [if (ord11≺ord21) [if (ord21≺ord12) (ord22≺OP ord12 ord13) [if (ord12≺ord21) (OP ord21 ord22≺ord13) (ord22≺ord13)]] (ord22≺OP ord12 ord13)]]∧ ¬[if (ord11≺ord21) [if (ord12≺ord21) (ord13≺OP ord21 ord22) [if (ord21≺ord12) (OP ord12 ord13≺ord22) (ord13≺ord22)]] [if (ord21≺ord11) (OP ord11(OP ord12 ord13)≺ord22) (OP ord12 ord13≺ord22)]]")
(assume "ord21" "ord11" "ord22" "ord12" "ord13")
(cut(pf"ord11~ord21∧OP ord12 ord13~ord22→OP ord11(OP ord12 ord13)~OP ord21 ord22"))
(search)
(use(pf"all ord1,ord2,ord3,ord4.
       (ord1~ord3∧ord2~ord4)→OP ord1 ord2~OP ord3 ord4"))
(search)
; Proof finished.
(nrw "ord11~ord21∧OP ord12 ord13≼ord22∧ord22≼OP ord12 ord13→ ¬[if (ord21≺ord11) (ord22≺OP ord11(OP ord12 ord13)) [if (ord11≺ord21) [if (ord21≺ord12) (ord22≺OP ord12 ord13) [if (ord12≺ord21) (OP ord21 ord22≺ord13) (ord22≺ord13)]] (ord22≺OP ord12 ord13)]]∧ ¬[if (ord11≺ord21) [if (ord12≺ord21) (ord13≺OP ord21 ord22) [if (ord21≺ord12) (OP ord12 ord13≺ord22) (ord13≺ord22)]] [if (ord21≺ord11) (OP ord11(OP ord12 ord13)≺ord22) (OP ord12 ord13≺ord22)]]")



)



(display"

Even more RW-rules

")


(begin


(sg "OPøord2~ ω⋆ord→ord2~ ω⋆ord")

(cases)
(auto)
; Proof finished.
(nrw "OPøord22~ ω⋆ord→ord22~ ω⋆ord")


(sg "¬(OPøord2~ ω⋆ord∧ord2≺ ω)")
(assume "ord" "ord2")
(cd "ord2≺ ω" "2<w")
(cd "OPøord2~ ω⋆ord" "1+2=wa")
(ng)
(simp "<-" (pf"(OPøord2~ ω⋆ord)=F"))
(use "1+2=wa")
(simp (pf"ord= ø"))
(use "Truth-Axiom")
(simp(pf"(ord= ø)=(ω⋆ord ≺ ω)"))
(booleimp "ω⋆ord ≼ OPøord2  ∧  OPøord2 ≺ ω")
(use (pf "all ord1,ord2.ord2≼ord1 ∧ ord1≺ ω → ord2≺ ω"))
(search)
(simp-with "1+2=wa" 'right)
(auto)
; Proof finished.
(nrw "¬(OPøord22~ ω⋆ord∧ord22≺ ω)")




(sg "(ord1≺ ω ∧ ord1≼ord2∧ord2≼ord1) →  ord1=ord2")
(ind)
    (assume "ord2")
    (simp "ordEQsym")
    (use "Truth-Axiom")
(assume "ord11" "ord12" "IH11" "IH12")
(ind)
(use "Truth-Axiom")
(assume "ord21" "ord22" "IH21" "IH22")
(ng #t)
(cds "ord11= ø" "11=0")
(ng #t)
(cds "ord21= ø" "21=0")
(ng #t)
(use-with "IH12" (pt"ord22"))
(assume "21≠0")
(ng #t)
(cd "ord12≺ ω" "12<w")
(simp(pf"ord12≺OP ord21 ord22"))
(use "Truth-Axiom")
(booleimp "ord12≺ ω ∧ ω ≼ OP ord21 ord22")
(use (pf"all ord1,ord2,ord3.ord1≺ord2 ∧ ord2≼ ord3 → ord1≺ord3"))
(search)
(simp "12<w")
(ng #t)
(simp "21≠0")
(auto)
; Proof finished.
(nrw "(ord1≺ ω ∧ ord1≼ord2 ∧ ord2≼ord1) →  ord1=ord2")


(sg "(ord2≺ ω ∧ ord1≼ord2 ∧ ord2≼ord1) →  ord1=ord2")
(assume "ord2" "ord1")
(ass "h")
(booleimp "ord1≺ ω ∧ord1≼ord2∧ord2≼ord1")
(use "Truth-Axiom")
(simp-with "h" 'right)
(simp-with "h" 'left 'right)
(booleimp "ord1≼ord2 ∧ ord2≺ ω")
(use "Truth-Axiom")
(simp-with "h" 'left 'right)
(use-with "h" 'left 'left)
; Proof finished.
(nrw "(ord2≺ ω ∧ ord1≼ord2 ∧ ord2≼ord1) →  ord1=ord2")



(display "

β ≺ ω   →    α ≼ β   =   α ≺ β ∨ α = β

")


(sg "ord2≺ ω → (ord1 ≼ ord2)=(ord1≺ord2 ∨ ord1=ord2)")
(assume "ord2" "ord1")
(ass "<w")
(cd "ord1≺ord2" "1<2")
    (ng)
    (simp "BooleTrueRight")
    (booleimp "ord1≺ord2")
    (auto)
    (assume "1≮2")
(cd "ord2≺ord1" "2<1")
    (ng)
    (cd "ord1=ord2" "1=2")
    (ng)
    (simp (pf"F=(ord2≺ord1)"))
    (use "2<1")
    (simp "1=2")
    (auto)
(assume "2≮1")
(ng)
(simp "BooleTrueLeft")
(booleimp "ord2≺ ω ∧ ord1≼ord2 ∧ ord2≼ord1")
(use "Truth-Axiom")
(simp "2≮1")
(simp "1≮2")
(use "<w")
; Proof finished.
(nrw "ord2≺ ω → (ord1 ≼ ord2)=(ord1≺ord2 ∨ ord1=ord2)")




(display "

α≺ ω   →   OP ø β ≼ α  =  β≺α
")

(sg "ord1≺ ω → (OP ø ord2 ≼ ord1)=(ord2≺ord1)")

(ind)
    (search)
(assume "ord11" "ord12" "IH11" "IH12")
(ind)
    (search)
(assume "ord21" "ord22" "IH21" "IH22")
(ass "<w")
(ca "ord12≺ ω" "12<w")
(cas "ord11= ø" "11=0")
(cd "OP ø ord12≺OPø(OP ord21 ord22)" "kl")
    (ng "kl" #t)
    (simp "BooleFalseLeft")
    (simp (pf"(OP ord21 ord22≺ord12)=F"))
    (cd "ord21= ø" "21=0")
	(ng #t)
	(simp "<-" (pf "(OPøord22≼ord12)=(ord22≺ord12)"))
	(ng #t)
	(simp "<-" "21=0")
	(auto)
	(booleimp "ord12≺ ω")
	(auto)
    (booleimp "ord12≺OP ord21 ord22")
    (auto)
(assume "(+)")
(ng "(+)" #t)
(simp "BooleTrueLeft")
(cas "ord21= ø" "21=0")
(ng #t)
(simp "<-" (pf "(OPøord22≼ord12)=(ord22≺ord12)"))
(simp "<-" "21=0")
(simp "(+)")
(use "Truth-Axiom")
(booleimp "ord12≺ ω")
(auto)
(booleimp "OP ord21 ord22≺ ω")
(use "Truth-Axiom")
(booleimp "OP ord21 ord22≼OP ord11 ord12 ∧ OP ord11 ord12≺ ω")
(use (pf"all ord1,ord2.ord1≼ord2∧ord2≺ ω →ord1≺ ω"))
(search)
(simp "<w")
(booleimp "OP ord21 ord22≼ord12 ∧ ord12≼OP ord11 ord12")
(use (pf"all ord1,ord2,ord3.ord1≼ord2∧ord2≼ord3 →ord1≼ord3∧ True"))
(search)
(simp "(+)")
(use "Truth-Axiom")
(booleimp "OP ord11 ord12≺ ω")
(auto)
(booleimp "ord12≼OP ord11 ord12 ∧ OP ord11 ord12≺ ω")
(auto)
; Proof finished.
(nrw "ord1≺ ω → (OP ø ord2 ≼ ord1)=(ord2≺ord1)")



(display "

ø ≠ β ≺ ω   →   α≺β = α⊏β

")

(sg "all ord2.(¬(ord2= ø) ∧ ord2≺ ω) → (ord1≺ord2)=(ord1⊏ord2)")

(cases)
    (cases)
    (auto)
(assume "ord11" "ord12")
(ind)
    (use "Truth-Axiom")
(assume "ord21" "ord22" "IH21" "IH22")
(drop "IH21")
(ass "hyp")
(ca "ord21= ø" "21=0")
(ca "ord22≺ ω" "22<w")
(cds "ord22= ø" "22=0")
    (simp "21=0")
    (use "Truth-Axiom")
(assume "22≠0")
(ca "(OP ord11 ord12≺ord22)=(OP ord11 ord12⊏ord22)" "IH22concl")
(drop "IH22")
(ca "¬(OP ord11 ord12=ord21) ∧ ¬(OP ord11 ord12⊏ord21)" "(*)")
(cds "OP ord11 ord12=ord22" "(11,12)=22")
    (simp "21=0")
    (ng #t)
    (simp "22<w")
    (use "Truth-Axiom")
(assume "(11,12)≠22")
(ng #t)
(simp "(11,12)≠22")
(ng #t)
(simp "(*)")
(simp (pf"(ord11≺ord21)=F"))
(ng #t)
(cd "ord21≺ord11" "21<11")
   (use "IH22concl")
(assume "21≮11")
(ng #t)
(cd "ord12≺ord22" "12<22")
    (simp "BooleTrueLeft")
    (simp "<-" "IH22concl")
    (cas "ord11= ø" "11=0")
    (simp(pf "(OPøord12≺ord22)=(OPøord12≼ord22)"))
    (simp(pf "(OPøord12≼ord22)=(ord12≺ord22)"))
    (use "12<22")
    (booleimp "ord22≺ ω")
    (auto)
    (simp(pf "(OPøord12≼ord22)=(OPøord12≺ord22 ∨ OPøord12=ord22)"))
    (simp(pf "(OPøord12=ord22)=F"))
    (use "Truth-Axiom")
    (simp "<-" "11=0")
    (simp "(11,12)≠22")
    (use "Truth-Axiom")
    (booleimp "ord22≺ ω")
    (auto)
    (booleimp "ord11≼ ø")
    (use "Truth-Axiom")
    (simp "<-" "21=0")
    (simp "21≮11")
    (use "Truth-Axiom")
(assume "12≮22")
(simp "BooleFalseLeft")
(simp "<-" "IH22concl")
(trans "ord12")
(simp "12≮22")
(use "Truth-Axiom")
(simp "21=0")
(auto)
(simp "21=0")
(auto)
(booleimp "¬(ord22= ø)∧ord22≺ ω")
(use "IH22")
(simp "22≠0")
(use "22<w")
(booleimp "ord22≼OP ord21 ord22 ∧ OP ord21 ord22≺ ω")
(auto)
(booleimp "OP ord21 ord22≺ ω")
(auto)
; Proof finished.
(nrw "(¬(ord2= ø) ∧ ord2≺ ω) → (ord1≺ord2)=(ord1⊏ord2)")
)


(display "

RW-rules involving ℧

")

(begin

(display "

ø ≺ ℧n

")
(sg "¬(℧ nat= ø)")
(cases)
(auto)
; Proof finished.
(trw "¬(℧ nat= ø)")



(display "

℧k ≺ ℧l  =  k < l

")
(sg "(℧nat1 ≺ ℧nat2)=(nat1<nat2)")
(ind)
    (cases)
    (auto)
(assume "nat1" "IH")
(cases)
(auto)
; Proof finished.
(arw "℧nat1 ≺ ℧nat2" "nat1<nat2")


(sg "(OP(℧nat1)ø ≼ ℧nat2)=(nat1<nat2)")
(cases)
(auto)
; Proof finished.
(arw "OP(℧nat1)ø ≼ ℧nat2" "nat1<nat2")




(sg "(ord1 ≺ ℧nat ∧ ord2 ≺ OP(℧nat)ø) → [if (ord1≺ ℧nat) (ord2≺OP(℧nat)ø) False]")
(assume "ord1" "nat" "ord2")
(ass "h")
(simp-with "h" 'left)
(simp-with "h" 'right)
(use "Truth-Axiom")
; Proof finished.
(nrw "(ord1 ≺ ℧nat ∧ ord2 ≺ OP(℧nat)ø) → [if (ord1≺ ℧nat) (ord2≺OP(℧nat)ø) False]")




(sg "ord1≺ ℧nat1∧nat1≤nat2→ord1≺ ℧nat2")
(assume "ord1" "nat1" "nat2")
(use-with (pf"all ord1,ord2,ord3.ord1≺ord2∧ord2≼ord3→ord1≺ord3")
          (pt"ord1") (pt"℧nat1") (pt"℧nat2"))
(search)
; Proof finished.
(nrw "ord1≺ ℧nat1∧nat1≤nat2→ord1≺ ℧nat2")



(sg "ord1≺OP(℧nat1)ø ∧nat1<nat2→ord1≺ ℧nat2")
(assume "ord1" "nat1" "nat2")
(use-with (pf"all ord1,ord2,ord3.ord1≺ord2∧ord2≼ord3→ord1≺ord3")
          (pt"ord1") (pt"OP(℧nat1)ø") (pt"℧nat2"))
(search)
; Proof finished.
(nrw "ord1≺OP(℧nat1)ø ∧nat1<nat2→ord1≺ ℧nat2")



(sg "(ord2≺OP(℧nat2)ø ∧ ℧nat2≺OP(℧nat1)ø) → ord2≺OP(OP(℧nat1)ø)ø")
(assume "ord2" "nat2" "nat1")
(use-with "ordSmallerTrans"
	  (pt"ord2") (pt"OP(℧nat2)ø") (pt"OP(OP(℧nat1)ø)ø"))
; Proof finished.
(nrw "(ord2≺OP(℧nat2)ø ∧ ℧nat2≺OP(℧nat1)ø) → ord2≺OP(OP(℧nat1)ø)ø")

)

(display "
Extraction of function MHO from

   ∃n α≺℧n

")

(begin

(sg "all ord.ex nat. ord ≺ ℧ nat ∧ ℧ nat ≼ ω^ ord")
(ind)
    (ex-intro (pt"0"))
    (use "Truth-Axiom")
(assume "ord1" "ord2" "IH1" "IH2")
(ex-elim "IH1")
(drop "IH1")
(cases)
    (ng)
    (assume "1=0")
    (simp "1=0")
    (ex-elim "IH2")
    (drop "IH2")
    (cases)
	(ng)
	(assume "2=0")
	(simp "2=0")
	(ex-intro(pt"1"))
	(use "Truth-Axiom")
    (assume "nat2" "ih2")
    (ex-intro(pt"SUCC nat2"))
    (ng)
    (simp-with "ih2" 'left)
    (ng)
    (trans "ord2")
    (use-with "ih2" 'right)
(assume "nat1" "ih1")
(ex-elim "IH2")
(drop "IH2")
(cases)
    (ng)
    (assume "2=0")
    (simp "2=0")
    (ex-intro(pt"SUCC(SUCC nat1)"))
    (search)
(assume "nat2" "ih2")
(cd "nat1<nat2" "1<2")
    (ex-intro (pt"SUCC nat2"))
    (ng)
    (simp (pf "ord1≺ ℧nat2"))
    (simp-with "ih2" 'left)
    (ng)
    (trans "ord2")
    (use-with "ih2" 'right)
    (booleimp "ord1≺ OP(℧nat1)ø ∧ OP(℧nat1)ø ≼ ℧nat2")
    (use "Truth-Axiom")
    (simp-with "ih1" 'left)
    (use "1<2")
(assume "1≮2")
(ex-intro(pt"SUCC(SUCC nat1)"))
(ng)
(simp-with "ih1" 'left)
(simp(pf "(ord1≺ ℧nat1)=F"))
(ng)
(trans "OP(℧nat2)ø")
(simp-with "ih2" 'left)
(ng)
(booleimp "℧nat2 ≼ ℧nat1 ∧ ℧nat1≺OP(℧nat1)ø")
(use "Truth-Axiom")
(ng)
(simp "1≮2")
(use "Truth-Axiom")
(simp "BooleFalseRight")
(use-with "ih1" 'right)
; Proof finished.
(save "MHO")
(display-theorems "MHO")

(test-extracted-unary "MHO")
)



(display "

End of hao_relations.scm
")

;EOF