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

changeset 1004:5c62c97adac9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
first cfcs done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 18 Nov 2022 19:37:18 +0900
parents b9dfe9bc8412
children 2808471040c0
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 18 18:14:41 2022 +0900
+++ b/src/zorn.agda	Fri Nov 18 19:37:18 2022 +0900
@@ -1082,10 +1082,10 @@
                       z53 = A∋fc {A} _ f mf fc
                       csupf1 : odef (UnionCF A f mf ay supf1 b) w
                       csupf1 with trio< (supf0 px) x
-                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx ? cp1 fc1 ⟫  where
+                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫  where
                           spx = supf0 px
-                          fc1 : FClosure A f (supf1 spx) w
-                          fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) ? ) fc
+                          spx≤px : supf0 px o≤ px
+                          spx≤px = zc-b<x _ sfpx<x
                           z54 :  {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (supf0 px)) z → (z ≡ supf0 px) ∨ (z << supf0 px)
                           z54 {z} ⟪ az , ch-init fc ⟫ = ZChain.fcy<sup zc o≤-refl fc
                           z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = subst (λ k → (z ≡ k) ∨ (z << k )) 
@@ -1099,16 +1099,18 @@
                           z52 : supf1 (supf0 px) ≡ supf0 px
                           z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.sup=u zc (ZChain.asupf zc) (zc-b<x _ sfpx<x) 
                                      ⟪ record { x≤sup = z54  } , ZChain.IsMinSUP→NotHasPrev zc (ZChain.asupf zc) z54 (( λ ax → proj1 (mf< _ ax))) ⟫ )
+                          fc1 : FClosure A f (supf1 spx) w
+                          fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
                           order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
                           order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 
-                                   (trans (sym (ZChain.supf-is-minsup zc ? )) (sym ? ) )
-                                   (MinSUP.x≤sup (ZChain.minsup zc ?) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
-                                       ? (fcup fcs ? ) ))
+                                   (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )
+                                   (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) 
+                                       spx≤px (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) )))
                           cp1 : ChainP A f mf ay supf1 spx
-                          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 ? )) 
-                                  ( ZChain.fcy<sup zc ? fc )
+                          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px )) 
+                                  ( ZChain.fcy<sup zc spx≤px fc )
                                        ; order =  order
-                                       ; supu=u = ? }
+                                       ; supu=u = z52 }
                       ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
                           -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
                           m12 : supf0 px ≡ sp1