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

changeset 1074:1e7d20b15341

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 Wed, 14 Dec 2022 12:18:48 +0900
parents b3d695340773
children 4e986bf9be8c
files src/zorn.agda
diffstat 1 files changed, 7 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Dec 14 11:21:16 2022 +0900
+++ b/src/zorn.agda	Wed Dec 14 12:18:48 2022 +0900
@@ -1473,15 +1473,18 @@
                supf0 = ZChain.supf (pzc (ob<x lim z<x)) 
                msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)
                msup = ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc)
+               s1=0 : {u : Ordinal } → u o< z → supf1 u ≡ supf0 u
+               s1=0 {u} u<z = trans (sf1=sf (ordtrans u<z z<x)) (zeq _ _ (o<→≤ (osucc u<z))  (o<→≤ <-osuc) ) 
                zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z 
-               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup  ⟪ az , ch-init fc ⟫ ) -- U supf0
+               zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) ( IsMinSUP.x≤sup msup  ⟪ az , ch-init fc ⟫ ) 
                zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf z<x)) 
-                  ( IsMinSUP.x≤sup msup  ⟪ az , ch-is-sup u u<b ? ? ⟫ ) -- U supf0
+                  ( IsMinSUP.x≤sup msup  ⟪ az , ch-is-sup u u<b (trans (sym (s1=0 u<b)) su=u)  (subst (λ k → FClosure A f k w) (s1=0 u<b) fc)  ⟫  )
                zm01 : { s : Ordinal } → odef A s →  ( {x : Ordinal  } → odef (UnionCF A f ay supf1 z) x → x ≤ s )  → supf1 z o≤ s
-               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where -- U supf1
+               zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup msup as zm02 ) where 
                    zm02 : {w : Ordinal } →  odef (UnionCF A f ay supf0 z) w → w ≤ s
                    zm02 {w} ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫
-                   zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup  ⟪ az , ch-is-sup u u<b ? ? ⟫
+                   zm02 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = sup  
+                       ⟪ az , ch-is-sup u u<b (trans (s1=0 u<b) su=u) (subst (λ k → FClosure A f k w) (sym (s1=0 u<b)) fc) ⟫