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

changeset 518:fc16a22225d9

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 Sat, 16 Apr 2022 18:14:48 +0900
parents 7b99c8944df7
children ef5dde91fa80
files src/zorn.agda
diffstat 1 files changed, 20 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Apr 16 16:09:14 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 18:14:48 2022 +0900
@@ -334,7 +334,26 @@
                 (subst (λ k → ic-connect (& k) (IChained.iy (proj2 zc5)) ) (me-elm-refl A x) (IChained.ic (proj2 zc5)) )  )
             zc6 : elm x < z
             zc6 = IsStrictPartialOrder.trans PO {x} {me (proj1 zc3)} {me az} zc7 y<z
-    ... | yes inifite = case2 (case2 record {    c-infinite = {!!}  } )
+    ... | yes inifite = case2 (case2 record {    c-infinite = zc9 } ) where
+        B : HOD
+        B = IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))
+        Nx : (y : Ordinal) → odef A y → HOD
+        Nx y ay = record { od = record { def = λ y → odef A y ∧ IChainSup> A (subst (λ k → odef A k) (sym &iso) ay)  } ; odmax = & A
+              ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A (proj1 lt)))  }
+        zc9 : (y : Ordinal) (cy : odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) y) →
+            IChainSup> A (ic→A∋y A (subst (OD.def (od A)) (sym &iso) (is-elm x)) cy)
+        zc9 y cy with  ODC.∋-p O (IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) (* y)
+        ... | no not = ⊥-elim (not (subst (λ k → odef (IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) k ) (sym &iso) cy))
+        ... | yes cy1  with is-o∅ (& (Nx y (proj1 cy) ))
+        ... | yes no-next = {!!} 
+        ... | no not = record { y = zc14 ; A∋y = IChainSup>.A∋y (proj2 zc12) ; y>x = zc15 } where
+                  zc13 = ODC.minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
+                  zc12 : odef A (& zc13 ) ∧ IChainSup> A (subst (λ k → odef A k) (sym &iso) (proj1 cy) )
+                  zc12 = ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
+                  zc14 : Ordinal
+                  zc14 = IChainSup>.y (proj2 zc12) 
+                  zc15 : * y < * ( IChainSup>.y (proj2 (ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq)))) )
+                  zc15 = IChainSup>.y>x (proj2 zc12)
 
 all-climb-case : { A : HOD } → (0<A : o∅ o< & A) → IsPartialOrderSet A
      → (( x : Element A) → OSup> A (d→∋ A (is-elm x) ))