;;; file:hao.scm

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


(display"
hao.scm is loading the following files

1) natnum.scm
2) unicode_formula.scm
3) hao_term.scm
4) hao_relations.scm
5) hao_equal.scm
6) hao_suc.scm
7) hao_cnf.scm

At the end you cantest the extracted
ordinal funcions by loading

hao_test.scm

")


(define (oload path) 
  (set! HAO-COMMENT-FLAG COMMENT-FLAG)
  (set! COMMENT-FLAG #f)
  (exload (string-append "ordinals/" path))
  (set! COMMENT-FLAG HAO-COMMENT-FLAG))


; Natnum Natural Numbers

(display"

The file natnum.scm introduces the natnum numbers
and proves some basic properties .

")

(oload "natnum.scm")
(mload "unicode_formula.scm")

(begin

(display"

The binary relation <

")
(display-program-constants "natLESS")
 
;;;;;;;;LESS is linear order ;;;;;;;

(display "

< is strict linear order:

")
(display "nat<nat                                  ")
    (pnt "nat<nat")
(display "nat1<nat2 ∧ nat2<nat1                   ")
    (pnt "nat1<nat2 ∧ nat2<nat1")
(display "(nat1<nat2 ∧ nat2<nat3) → (nat1<nat3)  ")
    (pnt "(nat1<nat2 ∧ nat2<nat3) → (nat1<nat3)")
(display "nat1<nat2 ∨ nat2<nat1 ∨ nat1=nat2      ")
(pnt(ORB "nat1<nat2" "nat2<nat1" "nat1=nat2"))

)





(display"

The file hao_term introduces the algebra ord.

")


(oload "hao_term.scm")

(begin

(display"

We define the algebra ord of Ordinals
as follows:

O ,   α,β  ->  ω^α + β

So we have:

    O : ø
    1 : OP NULL NULL
    2 : OP NULL (OP NULL NULL)
  n+1 : OP NULL n

   ω  : OP (OP NULL NULL) NULL
  ω+1 : OP (OP NULL NULL) (OP NULL NULL)
1+ω+1 : OP NULL (OP (OP NULL NULL) (OP NULL NULL))
  1+α : OP NULL α

")

(display "

subterm relation ⊏
")
(display-program-constants "subterm")
(newline)
(display-program-constants "ω⋆")
(newline)
(display-program-constants "ω^")
(display"

ω-Tower ℧
")
(display-program-constants "℧")
(newline)(newline)

(display-theorems "Comp")
(test-extracted-unary "Comp")

(display "
     ⊏ is transitive

ord1 ⊏ ord2  ∧  ord2 ⊏ ord3  →  ord1⊏ord3   : ")
(pnt "ord1 ⊏ ord2 ∧ ord2 ⊏ ord3  →  ord1⊏ord3")

(display "
We define inductively the prediacte FORD⊆ nat@ord
for finite ordinal.

and

extract an embedding of nat -> ord:

")
(animate "FO")

(display"

Test of cFO:

")
(display "cFO    1  = ")
(pnt "cFO 1")
(display "cFO   16  = ")
(pnt "cFO 16")
(newline)
(deanimate "FO")


(display "

Subterminduction:

    F^ ø  →  [ ∀α (∀β⊏α F^β) → F^ α ]  →  ∀γ F^ γ

")
(display-theorems  "STind")
)



(display"

The file hao_relations.scm defines
two binary relations ≺ and ≼ .

")

(oload "hao_relations.scm")

(begin

(display"

The binary relation ≺

")
(display-program-constants "SMALLER")

(display"

The binary relation ≼

")

(display-program-constants "LE")

 
; SMALLER is partial order ;;;;;;;

(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 "≼
")
(display "ord≼ord                                   ")
    (pnt "ord≼ord")
(display "(ord1≼ord2 ∧ ord2≼ord3) → (ord1≼ord3)  ")
    (pnt "(ord1≼ord2 ∧ ord2≼ord3) → (ord1≼ord3)")




(display"

The binary relation ~

")

(display-theorems"ICsym")

(display "(ord1~ord2 ∧ ord2~ord3) → ord1~ord3   :  ")
(pnt"(ord1~ord2 ∧ ord2~ord3) → ord1~ord3")
(display "ord1~ord2 ∨ ord1≺ord2 ∨ ord2≺ord1   :  ")
(pnt"ord1~ord2 ∨ ord1≺ord2 ∨ ord2≺ord1")


(display "equalsmaller
ord1~ord2 → ((ord3 ≺ ord1) = (ord3 ≺ ord2))   :  ")
(pnt"ord1~ord2 → ((ord3 ≺ ord1) = (ord3 ≺ ord2))")
(display"
equalslarger:
ord1~ord2 → ((ord1 ≺ ord3) = (ord1 ≺ ord3))   :  ")
(pnt "ord1~ord2 → ((ord1 ≺ ord3) = (ord1 ≺ ord3))")

(test-extracted-binary "minusexp")

(display-theorems "minusexp")
(display-theorems "minexp")
(display"
OPfunctional:
(ord1~ord3 ∧ ord2~ord4) → OP ord1 ord2 ~ OP ord3 ord4  :  ")
(pnt "(ord1~ord3 ∧ ord2~ord4) → OP ord1 ord2 ~ OP ord3 ord4")
(newline)

(test-extracted-unary "MHO")
)








(display"

In the next file we extract

cS    : successor
cPred : extended predecessor
cP    : predecessor
")

(oload "hao_suc.scm")

(begin

(test-extracted-unary "S")
(test-extracted-unary "Pred")
(test-extracted-unary "P")

)


(display"

The file hao_cnf.scm defines
normality of a term:

N: ord -> boole

and extracts

cnf   : Cantor-Normal-Form

")


(oload "hao_cnf.scm")


(begin

(newline)(newline)
(display"Normality of a term
as boolean valued function.")
(newline)(newline)
(display-program-constants "N")
(newline)(newline)
(display"There is only one normal term :

   (ord1~ord2 ∧ N ord1 ∧ N ord2) → (ord1=ord2)   ")
(pnt "(ord1~ord2 ∧ N ord1 ∧ N ord2) → (ord1=ord2)")
(display"

The height of an ordinal term
ht : ord -> nat")
(newline)(newline)
(display-program-constants "ht")
(newline)(newline)
(display" Extracted Cantor-Normal-Form
 
  ex ord2.ord1~ord2 ∧ N ord2")
(newline)(newline)
(animate "Comp")
(test-extracted-unary "nf")
(deanimate "Comp")
(newline)(newline)
(display "The Cantor-Normal-Form is normal :

   N(cnf ord) ∧ cnf ord ~ ord     ")
(pnt  "N(cnf ord) ∧ cnf ord ~ ord")
(newline)(newline)
(display " There is a unique term in CNF

   cnf ord1 ~ cnf ord2  →  cnf ord1 = cnf ord2     ")
(pnt "cnf ord1 ~ cnf ord2 → cnf ord1 = cnf ord2")
(newline)
(display "       ord1 ~ ord       →  cnf ord1 = cnf ord2     ")
(pnt "ord1 ~ ord2 → cnf ord1 = cnf ord2")


)



(set! HAO-COMMENT-FLAG COMMENT-FLAG)
(set! COMMENT-FLAG #t)
(display "


  GLOBAL ASSUMPTIONS
")
(display-global-assumptions)
(display"


          ACKNOWLEDGMENTS

Markus Sauermann
for his idea to introduce 'term'-constants

Oliver Deiser
for Bonsai

Stefan Schimanski
for his help concerning Scheme programming and idea concerning ordinals.


signed:
Klaus Thiel
Ludwig-Maximilians-Universität
München (Germany), März 2004
")

(set! COMMENT-FLAG HAO-COMMENT-FLAG)

; EOF