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

changeset 1008:47c0f8fa7b0c

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 Sun, 20 Nov 2022 09:29:56 +0900
parents 88fae58f89f5
children 7c39cae23803
files src/zorn.agda
diffstat 1 files changed, 20 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Nov 20 08:36:24 2022 +0900
+++ b/src/zorn.agda	Sun Nov 20 09:29:56 2022 +0900
@@ -532,25 +532,33 @@
        supfa = ZChain.supf za
        supfb = ZChain.supf zb
        ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x
-       ind x prev x≤xa = ? where
-           sax=m : supfa x ≡ MinSUP.sup (ZChain.minsup za x≤xa )
-           sax=m = ZChain.supf-is-minsup za x≤xa 
-           sbx=m : supfb x ≡ MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))
-           sbx=m = ZChain.supf-is-minsup zb (OrdTrans x≤xa xa≤xb )
+       ind x prev x≤xa = sxa=sxb where
+           ma = ZChain.minsup za x≤xa 
+           mb = ZChain.minsup zb (OrdTrans x≤xa xa≤xb )
+           spa = MinSUP.sup ma
+           spb = MinSUP.sup mb
+           sax=spa : supfa x ≡ spa
+           sax=spa = ZChain.supf-is-minsup za x≤xa 
+           sbx=spb : supfb x ≡ spb
+           sbx=spb = ZChain.supf-is-minsup zb (OrdTrans x≤xa xa≤xb )
            sxa=sxb : supfa x ≡ supfb x
            sxa=sxb with trio< (supfa x) (supfb x)
            ... | tri≈ ¬a b ¬c = b
            ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (
                begin
-                 supfb x  ≡⟨ ? ⟩
-                 MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))  ≤⟨ MinSUP.minsup ? ? ? ⟩
-                 MinSUP.sup (ZChain.minsup za x≤xa ) ≡⟨ ? ⟩ 
-                 supfa x ∎ ) a ) where open o≤-Reasoning O
+                 supfb x  ≡⟨ sbx=spb ⟩
+                 spb  ≤⟨ MinSUP.minsup mb (MinSUP.asm ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩
+                 spa ≡⟨ sym sax=spa ⟩ 
+                 supfa x ∎ ) a ) where 
+                    open o≤-Reasoning O
+                    z53 : {z : Ordinal } →  odef (UnionCF A f mf ay (ZChain.supf zb) x) z →  odef (UnionCF A f mf ay (ZChain.supf za) x) z
+                    z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
+                    z53 ⟪ as , ch-is-sup u u<x is-sup fc ⟫ =  ⟪ as , ch-is-sup u u<x ? ?  ⟫ 
            ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
                begin
-                 supfa x  ≡⟨ ? ⟩
-                 MinSUP.sup (ZChain.minsup za x≤xa )  ≤⟨ MinSUP.minsup ? ? ? ⟩
-                 MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))  ≡⟨ ? ⟩
+                 supfa x  ≡⟨ sax=spa ⟩
+                 spa  ≤⟨ MinSUP.minsup ma (MinSUP.asm mb) (λ uza → MinSUP.x≤sup mb ?) ⟩
+                 spb  ≡⟨ sym sbx=spb ⟩
                  supfb x ∎ ) c ) where open o≤-Reasoning O
 
 UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)