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

changeset 677:be3eb95d50d9

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, 09 Jul 2022 17:23:41 +0900
parents 9ab62416dbdd
children fca33c0e9a88
files src/zorn.agda
diffstat 1 files changed, 4 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Jul 09 17:10:50 2022 +0900
+++ b/src/zorn.agda	Sat Jul 09 17:23:41 2022 +0900
@@ -262,8 +262,9 @@
    field
       psup :  Ordinal → Ordinal 
       psup<z : (x : Ordinal ) →   psup x o< & A 
-      chainf : (x w : Ordinal) → x o< z  →  Chain A f mf ay (psup x ) w
-      psup-mono : (x y : Ordinal) → x o≤ y → psup x o≤ psup y 
+      chainf : (x : Ordinal) → x o< z  →  HOD
+      is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x x<z ) w → Chain A f mf ay (psup x ) w 
+      psup-mono : (x y : Ordinal) → x o≤ y → chainf x ? ⊆' chainf y ? 
 
 ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) 
      → (z : Ordinal) →  ( ( x : Ordinal ) → ZChain1 A f mf ay x ) →  HOD
@@ -503,33 +504,7 @@
           no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain (zc z<x )) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain (zc z<x) ) ab f ∨  IsSup A (ZChain.chain (zc z<x) ) ab →
                             * a < * b → odef (ZChain.chain (zc ?) ) b ) → ZChain A f mf ay zc0 x
-          no-extenion is-max with o≤? x (& A)
-          ... | no n = ? where
-          ... | yes x≤a with ZChain1.chainf (zc0 (& A)) ?  ? ?
-          ... | ch-init _ _  x=0 fc = ?
-          ... | ch-is-sup ax is-sup fc = ? where
-          -- = record { chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
-          --           ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc)
-          --           ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc) 
-          --           ; f-total = {!!} 
-          --           ; chain∋init  = subst (λ k → odef k y ) {!!} (ZChain.chain∋init  zc) 
-          --           ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
-          --                       HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) {!!} is-max } where
-                supf0 : Ordinal → HOD
-                supf0 z with trio< z x
-                ... | tri< a ¬b ¬c = ?
-                ... | tri≈ ¬a b ¬c = ZChain.chain (zc ?)
-                ... | tri> ¬a ¬b c = ZChain.chain (zc ?)
-                seq : ZChain.chain (zc ?) ≡ supf0 x 
-                seq with trio< x x
-                ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-                ... | tri≈ ¬a b ¬c = refl 
-                ... | tri> ¬a ¬b c = refl 
-                seq<x : {b : Ordinal } → b o< x →  ? -- supf b  ≡ supf0 b
-                seq<x {b} b<x with trio< b x
-                ... | tri< a ¬b ¬c = refl
-                ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
-                ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
+          no-extenion is-max = ? 
 
           zc4 : ZChain A f mf ay zc0 x 
           zc4 with o≤? x o∅