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

changeset 716:b0cad3ec7da0

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 Fri, 15 Jul 2022 21:39:32 +0900
parents e4587714c376
children d76047a8a89b 6c9fed204440
files src/zorn.agda
diffstat 1 files changed, 12 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 15 14:14:53 2022 +0900
+++ b/src/zorn.agda	Fri Jul 15 21:39:32 2022 +0900
@@ -497,6 +497,11 @@
           imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
           imax {a} {b} ua b<x ab (case2 sup)  a<b = ⊥-elim ( ¬x<0 b<x )
 
+     -- exor-sup : (B : HOD) 
+     --    → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → 
+     --    → {x : Ordinal } (xa : odef A x) → HasPrev A B xa → IsSup A B xa → ⊥
+     -- exor-sup B f mf {y} ay {x} xa hasp is-sup with trio< 
+
      --
      -- create all ZChains under o< x
      --
@@ -619,8 +624,14 @@
                       ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
                       zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ with trio< u px
                       ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 
-                      ... | tri≈ ¬a b ¬c = ? -- ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans b (sym &iso) )  (ChainP.au is-sup ) ))
                       ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
+                      ... | tri≈ ¬a b ¬c = ? where
+                          zc13 : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) (HasPrev.y pr)
+                          zc13 = HasPrev.ay pr 
+                          zc12 : ?
+                          zc12 with proj1 (mf _ (A∋fcs _ f mf fc ) ) | zc13  -- u is sup and has prev
+                          ... | case1 x | ⟪ apz , ach ⟫ = ?
+                          ... | case2 x | ⟪ apz , ach ⟫ = ?
                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
                 ... | tri≈ ¬a b=px ¬c = zc15 where
                        zc14 : f (HasPrev.y pr) ≡ b