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

comparison src/zorn.agda @ 1037:23e185ef2737

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, 02 Dec 2022 19:14:41 +0900
parents 23a8e4d558e0
children dfbac4b59bae
comparison
equal deleted inserted replaced
1036:23a8e4d558e0 1037:23e185ef2737
1055 ... | case2 fc = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (case2 fc) ) 1055 ... | case2 fc = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (case2 fc) )
1056 z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s ) 1056 z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s )
1057 → supf1 z o≤ s 1057 → supf1 z o≤ s
1058 z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where 1058 z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where
1059 z25 : {w : Ordinal } → odef pchainpx w → w ≤ s 1059 z25 : {w : Ordinal } → odef pchainpx w → w ≤ s
1060 z25 {w} (case2 fc) = sup ⟪ ? , ch-is-sup px px<z z27 (fcpu fc ?) ⟫ where 1060 z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) ? ? ? ⟫ where
1061 z27 : supf1 px ≡ px --- sp1 o≤ x 1061 z27 : supf1 px ≡ px --- sp1 o≤ x
1062 z27 = ? 1062 z27 = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc ? ? ? )
1063 z29 : supf0 px o≤ z
1064 z29 = ? -- supf0 px ≡ supf1 px o≤ supf1 x o≤ x ≡ z
1065 z28 : supf0 px o< z
1066 z28 = ?
1063 z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫ 1067 z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫
1064 z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫) = sup ⟪ ua , ch-is-sup u u<z 1068 z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫) = sup ⟪ ua , ch-is-sup u u<z
1065 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where 1069 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where
1066 u≤px : u o< osuc px 1070 u≤px : u o< osuc px
1067 u≤px = ordtrans u<x <-osuc 1071 u≤px = ordtrans u<x <-osuc