Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 83:e013ccf00567

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jun 2019 12:28:43 +0900
parents 57814596a986
children 4b2aff372b7c
files ordinal-definable.agda
diffstat 1 files changed, 23 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Tue Jun 04 09:22:45 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 04 12:28:43 2019 +0900
@@ -343,14 +343,31 @@
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
-         pair-is-u : (x y : OD) → Union (x , y) ==  (x , y )
-         eq→ (pair-is-u x y) {w} z = def-subst (o<→c< ( ordtrans <-osuc z )) oiso diso
-         eq← (pair-is-u x y) {w} (case1 refl) =
-             def-subst (union→ (x , y) (ord→od w) (ord→od (osuc w)) ( record { proj1 = {!!} ; proj2 = {!!} } )) refl diso
-         eq← (pair-is-u x y) {w} (case2 refl) = {!!}
+         pair-or : {x y : OD {suc n} } → (x , x) ∋ y → (y == x ) ∨ (x ∋ y )
+         pair-or {x} {y} lt with tri-c< x y
+         pair-or {x} {y} lt | tri< a ¬b ¬c = {!!}   --     x < y < ( x ,  x )
+         pair-or {x} {y} lt | tri≈ ¬a b ¬c = case1 (eq-sym b)
+         pair-or {x} {y} lt | tri> ¬a ¬b c = case2 c
+         pair-osuc : (x : OD) →  od→ord (x , x) ≡ osuc (od→ord x)
+         pair-osuc x with trio< (od→ord (x , x)) (osuc (od→ord x))
+         pair-osuc x | tri< a ¬b ¬c = ⊥-elim ( osuc-<  a (c<→o< (proj1 (pair x x )) ))
+         pair-osuc x | tri≈ ¬a b ¬c = b
+         pair-osuc x | tri> ¬a ¬b c with pair-or (def-subst (o<→c<  c ) oiso refl ) --  (x , x)  ∋ ord→od (osuc (od→ord x) )
+         pair-osuc x | tri> ¬a ¬b c | case1 eq = ⊥-elim ( o<→¬== (def-subst {suc n} (o<→c<  c ) refl diso ) eq )
+         pair-osuc x | tri> ¬a ¬b c | case2 lt = ⊥-elim (c<> c lt ) where
+             lemma2 : (z : Ordinal {suc n} ) → lv (od→ord (ord→od z , ord→od z) ) ≡ lv z
+             lemma2 z = {!!}
          next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
          eq→ (next x ) {y} z = {!!}
-         eq← (next x ) {y} z = {!!}
+         eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_}
+                  (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where
+             lemma1 : (x , (x , x)) ∋ ord→od (osuc y)    -- z : def (ord→od (osuc (od→ord x))) y
+             lemma1 with tri-c< (x , x) (ord→od (osuc (od→ord x)))
+             lemma1 | tri< a ¬b ¬c = {!!}
+             lemma1 | tri≈ ¬a b ¬c = {!!}
+             lemma1 | tri> ¬a ¬b c = {!!}
+             lemma2 : ord→od (osuc y) ∋ ord→od y
+             lemma2 = o<→c< <-osuc
          next' : (x : OD) →  ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x))
          next' x = subst ( λ k → k == ord→od (osuc (od→ord x))) (sym oiso) (next x)
          infinite : OD {suc n}