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

changeset 726:b2e2cd12e38f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
psupf-mono and is-max conflict
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 18 Jul 2022 15:30:35 +0900
parents 3c42f0441bbc
children 322dd6569072
files src/zorn.agda
diffstat 1 files changed, 17 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 18 11:50:52 2022 +0900
+++ b/src/zorn.agda	Mon Jul 18 15:30:35 2022 +0900
@@ -679,15 +679,29 @@
                    sup1 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
                    sup1 {z} uz = IsSup.x<sup b=sup ( chain-mono uz  )
      ... | no op = zc5 where
+
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
+
           psupf0 : (z : Ordinal) → Ordinal
           psupf0 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
           ... | tri≈ ¬a b ¬c = y
           ... | tri> ¬a ¬b c = y
+
           pchain : HOD
           pchain = UnionCF A f mf ay psupf0 x
+
+          psupf0=pzc : {z : Ordinal} → (z<x : z o< x) → psupf0 z ≡ ZChain.supf (pzc z z<x) z
+          psupf0=pzc {z} z<x with trio< z x
+          ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
+          ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
+          ... | tri< a ¬b ¬c with o<-irr z<x a 
+          ... | refl = refl
+
+          psupf-mono : {z x1 : Ordinal} → (z<x1 : z o< x1) → x1 o≤ x → psupf0 z ≡ ZChain.supf (pzc z z<x1) z
+          psupf-mono {z} z<x1 x1≤x =?
+
           ptotal : IsTotalOrderSet pchain
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
@@ -757,9 +771,10 @@
                ⟪ ab , record { u = x=0 ; u<x = case2 refl ; uchain = ch-init b fc } ⟫ 
           uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case2 x=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ?
           uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
-               ⟪ ab , record { u = u ; u<x = case1 (ordtrans u<x ob<x) ; uchain = ch-is-sup uzc00 (fc-conv {b} {u} {ZChain.supf (prev (osuc b) ob<x)} {psupf0} uzc01 fc) } ⟫ where
+               ⟪ ab , record { u = u ; u<x = case1 (ordtrans u<x ob<x) ; uchain = ch-is-sup uzc00 
+                       (fc-conv {b} {u} {ZChain.supf (prev (osuc b) ob<x)} {psupf0} uzc01 fc) } ⟫ where
                    uzc01 : ZChain.supf (prev (osuc b) ob<x) u  ≡ psupf0 u
-                   uzc01 = ?
+                   uzc01 = ? -- trans (sym (psupf0=pzc (ordtrans u<x ob<x ) )) ?
                    uzc00 : ChainP A f mf ay psupf0 u b
                    uzc00 = ?