Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 81:96c932d0145d
simpler ordinal
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 04 Jun 2019 01:05:33 +0900 |
| parents | 714470702a8b |
| children | 4b2aff372b7c |
line wrap: on
line diff
--- a/ordinal.agda Mon Jun 03 12:29:33 2019 +0900 +++ b/ordinal.agda Tue Jun 04 01:05:33 2019 +0900 @@ -11,27 +11,18 @@ data OrdinalD {n : Level} : (lv : Nat) → Set n where Φ : (lv : Nat) → OrdinalD lv OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv - ℵ_ : (lv : Nat) → OrdinalD (Suc lv) record Ordinal {n : Level} : Set n where field lv : Nat ord : OrdinalD {n} lv -data ¬ℵ {n : Level} {lx : Nat } : ( x : OrdinalD {n} lx ) → Set where - ¬ℵΦ : ¬ℵ (Φ lx) - ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x) - -- -- Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ... < ℵ (Suc lv) -- data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y - ℵΦ< : {lx : Nat} → Φ (Suc lx) d< (ℵ lx) - ℵ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x → OSuc (Suc lx) x d< (ℵ lx) - ℵs< : {lx : Nat} → (ℵ lx) d< OSuc (Suc lx) (ℵ lx) - ℵss< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → (ℵ lx) d< x → (ℵ lx) d< OSuc (Suc lx) x open Ordinal @@ -41,26 +32,14 @@ s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x s<refl {n} {lv} {Φ lv} = Φ< s<refl {n} {lv} {OSuc lv x} = s< s<refl -s<refl {n} {Suc lv} {ℵ lv} = ℵs< trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t -trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ()) -trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs< trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< () -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ()) -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y -trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ) -trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x) d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y d<→lv Φ< = refl d<→lv (s< lt) = refl -d<→lv ℵΦ< = refl -d<→lv (ℵ< _) = refl -d<→lv ℵs< = refl -d<→lv (ℵss< _) = refl o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x o<-subst df refl refl = df @@ -99,25 +78,10 @@ triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly ) triO {n} {lx} {ly} x y = <-cmp lx ly -fin : {n : Level} → {lx : Nat} → {y : OrdinalD {n} (Suc lx) } → y d< (ℵ lx) → ¬ℵ y -fin {_} {_} {Φ (Suc _)} ℵΦ< = ¬ℵΦ -fin {_} {_} {OSuc (Suc _) _} (ℵ< x) = ¬ℵs x - triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< -triOrdd {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d< triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) -triOrdd {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri< ℵΦ< (λ ()) ( λ lt → trio<> lt ℵΦ<) -triOrdd {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt ℵΦ< ) (λ ()) ℵΦ< -triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y ) with triOrdd (ℵ lv) y -triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri< a ¬b ¬c = tri< (ℵss< a) (λ ()) (trio<> (ℵss< a) ) -triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri≈ ¬a refl ¬c = tri< ℵs< (λ ()) ( λ lt → trio<> lt ℵs< ) -triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt ( ℵ< (fin c)) ) (λ ()) ( ℵ< (fin c) ) triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) with triOrdd x (ℵ lv) -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri< a ¬b ¬c = tri< (ℵ< (fin a ) ) (λ ()) ( λ lt → trio<> lt (ℵ< (fin a ))) -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri≈ ¬a refl ¬c = tri> (λ lt → trio<> lt ℵs< ) (λ ()) ℵs< -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri> ¬a ¬b c = tri> (λ lt → trio<> lt (ℵss< c )) (λ ()) ( ℵss< c ) triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) ) triOrdd {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d< @@ -129,7 +93,6 @@ <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x <-osuc {n} {record { lv = lx ; ord = Φ .lx }} = case2 Φ< <-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl ) -<-osuc {n} {record { lv = (Suc lx) ; ord = ℵ lx }} = case2 ℵs< osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x ) osuc-lveq {n} = refl @@ -140,73 +103,43 @@ nat-<≡ : { x : Nat } → x < x → ⊥ nat-<≡ (s≤s lt) = nat-<≡ lt +nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ +nat-≡< refl lt = nat-<≡ lt + ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ ¬a≤a (s≤s lt) = ¬a≤a lt -xsyℵ : {n : Level} {lx : Nat} {x y : OrdinalD {n} lx } → x d< y → ¬ℵ y → ¬ℵ x -xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ -xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t) -xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) () -xsyℵ {_} {_} {ℵ lv₁} {.(OSuc (Suc lv₁) (ℵ lv₁))} ℵs< (¬ℵs t) = t -xsyℵ (ℵss< ()) (¬ℵs ¬ℵΦ) -xsyℵ (ℵss< x<y) (¬ℵs t) = xsyℵ x<y t +o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥ +o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<> x₁ x₂ +o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁ +o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂ +o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ()) +o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = + o<> (case2 y<x) (case2 x<y) orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< -orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ< orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) -orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) (Φ (Suc lx)))} {.(ℵ lx)} (s< ()) (ℵ< ¬ℵΦ) -orddtrans ℵs< (ℵ< ()) -orddtrans {n} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc ly) y} {ℵ _} (s< x<y) (ℵ< t) = ℵ< ( xsyℵ x<y t ) -orddtrans {n} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} ℵΦ< ℵs< = Φ< -orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s< ℵΦ< -orddtrans {n} {.(Suc _)} {OSuc (Suc lv) (OSuc (Suc _) x)} {ℵ lv} {.(OSuc (Suc _) (ℵ _))} (ℵ< (¬ℵs t)) ℵs< = s< ( ℵ< t ) -orddtrans {n} {.(Suc lv)} {ℵ lv} {OSuc .(Suc lv) (ℵ lv)} {OSuc .(Suc lv) .(OSuc (Suc lv) (ℵ lv))} ℵs< (s< ℵs<) = ℵss< ℵs< -orddtrans ℵΦ< (ℵss< y<z) = Φ< -orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans ℵΦ< y<z) -orddtrans (ℵ< {lx} {OSuc .(Suc lx) xx} (¬ℵs nxx)) (ℵss< y<z) = s< (orddtrans (ℵ< nxx) y<z) -orddtrans (ℵ< {.lv₁} {ℵ lv₁} ()) (ℵss< y<z) -orddtrans (ℵss< x<y) (s< y<z) = ℵss< ( orddtrans x<y y<z ) -orddtrans (ℵss< ()) (ℵ< ¬ℵΦ) -orddtrans (ℵss< ℵs<) (ℵ< (¬ℵs ())) -orddtrans (ℵss< (ℵss< x<y)) (ℵ< (¬ℵs x)) = orddtrans (ℵss< x<y) ( ℵ< x ) -orddtrans {n} {Suc lx} {x} {y} {z} ℵs< (s< (ℵss< {lx} {ss} y<z)) = ℵss< ( ℵss< y<z ) osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a) osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt) osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case1 refl osuc-≡< {n} {record { lv = lv₁ ; ord = OSuc .lv₁ ord₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case2 (case2 Φ<) -osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) }} (case2 Φ<) = case2 (case2 ℵΦ<) osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< ())) osuc-≡< {n} {record { lv = la ; ord = OSuc la oa }} {record { lv = la ; ord = (OSuc la ox) }} (case2 (s< lt)) with osuc-≡< {n} {record { lv = la ; ord = oa }} {record { lv = la ; ord = ox }} (case2 lt ) ... | case1 refl = case1 refl ... | case2 (case2 x) = case2 (case2( s< x) ) ... | case2 (case1 x) = ⊥-elim (¬a≤a x) where -osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) (Φ (Suc lv₁))) }} (case2 (s< ℵΦ<)) = case2 (case2 (ℵ< ¬ℵΦ )) -osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) (OSuc (Suc lx) ox)) }} (case2 (s< (ℵ< x))) with - osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) ox) }} (case2 (lemma (ℵ< x)) ) where - lemma : OSuc (Suc lx) ox d< (ℵ lx) → OSuc (Suc lx) ox d< ord (osuc (record { lv = Suc lx ; ord = ℵ lx })) - lemma lt = orddtrans lt s<refl -... | case1 () -... | case2 ttt = case2 ( case2 (ℵ< (¬ℵs x) )) -osuc-≡< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 ℵs<) = case1 refl -osuc-≡< {n} {record { lv = .(Suc _) ; ord = Φ .(Suc _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt) -osuc-≡< {n} {record { lv = .(Suc _) ; ord = OSuc .(Suc _) ord₁ }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt) -osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(ℵ lv₁) }} (case2 (ℵss< lt)) = case1 refl osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ osuc-< {n} {x} {y} y<ox x<y with osuc-≡< y<ox osuc-< {n} {x} {x} y<ox (case1 x₁) | case1 refl = ⊥-elim (¬a≤a x₁) osuc-< {n} {x} {x} (case1 x₂) (case2 x₁) | case1 refl = ⊥-elim (¬a≤a x₂) osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d< x₁ -osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₁ x₂ -osuc-< {n} {x} {y} y<ox (case2 x₂) | case2 (case1 x₁) with d<→lv x₂ -... | refl = ⊥-elim (¬a≤a x₁) -osuc-< {n} {x} {y} y<ox (case1 x₁) | case2 (case2 y<x) with d<→lv y<x -... | refl = ⊥-elim (¬a≤a x₁) -osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 (case2 y<x) with d<→lv y<x | d<→lv x<y -... | refl | refl = trio<> y<x x<y +osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₂ x₁ +osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case2 x₁) = nat-≡< (sym (d<→lv x₁)) x₂ +osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 y<x = o<> (case2 x<y) y<x max : (x y : Nat) → Nat max Zero Zero = Zero @@ -231,26 +164,23 @@ ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ ) -ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂ +ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂ ... | refl = case1 x₁ -ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁ +ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁ ... | refl = case1 x₂ ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂ ... | refl | refl = case2 ( orddtrans x₁ x₂ ) - trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_ trio< a b with <-cmp (lv a) (lv b) trio< a b | tri< a₁ ¬b ¬c = tri< (case1 a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a) lemma1 (case1 x) = ¬c x - lemma1 (case2 x) with d<→lv x - lemma1 (case2 x) | refl = ¬b refl + lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) a₁ ) trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b) lemma1 (case1 x) = ¬a x - lemma1 (case2 x) with d<→lv x - lemma1 (case2 x) | refl = ¬b refl + lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) c ) trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b ) trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b @@ -273,13 +203,7 @@ OrdTrans (case1 refl) (case1 refl) = case1 refl OrdTrans (case1 refl) (case2 lt2) = case2 lt2 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 -OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) ) -OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y -OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x ) -OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x -OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y) -OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y -OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y )) +OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n) OrdPreorder {n} = record { Carrier = Ordinal @@ -293,12 +217,9 @@ } TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n } - → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) → ∀ (x : Ordinal) → ψ x -TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv -TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁ - ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } )) -TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁ - +TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv +TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = + caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox })