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

comparison src/zorn.agda @ 1052:0b6cee971cba

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, 09 Dec 2022 11:38:13 +0900
parents 8d25e368e26f
children a281ad683577
comparison
equal deleted inserted replaced
1051:8d25e368e26f 1052:0b6cee971cba
472 472
473 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b 473 supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b
474 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) 474 supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl)
475 ... | case2 lt = lt 475 ... | case2 lt = lt
476 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) 476 ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
477
478 supfeq : {a b : Ordinal } → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b
479 supfeq = ?
480
481 unioneq : {a b : Ordinal } → z o≤ supf a → supf a o≤ supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
482 unioneq = ?
477 483
478 -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b) 484 -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b)
479 -- the condition of cfcs is satisfied, this is obvious 485 -- the condition of cfcs is satisfied, this is obvious
480 486
481 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) 487 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f)
1187 a≤px with trio< a px 1193 a≤px with trio< a px
1188 ... | tri< a ¬b ¬c = o<→≤ a 1194 ... | tri< a ¬b ¬c = o<→≤ a
1189 ... | tri≈ ¬a b ¬c = o≤-refl0 b 1195 ... | tri≈ ¬a b ¬c = o≤-refl0 b
1190 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k) (sym (Oprev.oprev=x op)) 1196 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k) (sym (Oprev.oprev=x op))
1191 ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x 1197 ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x
1192 spx<x : supf0 px o< x
1193 spx<x = ?
1194 spx<=sb : supf0 px ≤ sp1
1195 spx<=sb = MinSUP.x≤sup sup1 (case2 ⟪ init (ZChain.asupf zc) refl , ? ⟫ )
1196 sa<<sb : supf1 a << supf1 b
1197 sa<<sb with osuc-≡< b≤x
1198 ... | case2 b<x = subst₂ (λ j k → j << k ) (sym (sf1=sf0 ?)) (sym (sf1=sf0 ?)) ( ZChain.supf-mono< zc (zc-b<x _ b<x)
1199 (subst₂ (λ j k → j o< k) (sf1=sf0 ?) (sf1=sf0 ?) sa<sb ))
1200 ... | case1 b=x with osuc-≡< ( supf1-mono a≤px ) -- supf1 a ≤ supf1 px << sp1
1201 ... | case2 sa<spx = subst₂ (λ j k → j << k ) (sym (sf1=sf0 ?)) (sym (sf1=sp1 ?))
1202 ( ftrans<-≤ ( ZChain.supf-mono< zc o≤-refl (subst₂ (λ j k → j o< k) (sf1=sf0 ?) (sf1=sf0 ?) sa<spx)) spx<=sb )
1203 ... | case1 sa=spx with spx<=sb
1204 ... | case2 lt = subst₂ (λ j k → j << k ) ? ? lt
1205 ... | case1 eq = ?
1206 -- supf1 a o≤ x
1207 -- x o< supf1 a o< supf1 b -> UnionCF px ⊆ UnionCF a → supf0 px ≡ supf0 a → ⊥
1208 -- a o≤ supf1 a
1209 sa<x : supf1 a o< x -- supf1 a o< supf1 x ≡ sp1 ( supf of fc (supf0 px) ∧ (supf0 px o< x)
1210 sa<x with x<y∨y≤x (supf1 a) x
1211 ... | case1 lt = lt
1212 ... | case2 x≤sa = ⊥-elim ( <<-irr z27 sa<<sb ) where
1213 z27 : supf1 b ≤ supf1 a
1214 z27 = subst (λ k → supf1 b ≤ k ) ? (IsMinSUP.x≤sup (is-minsup ? ) ? )
1215 ssa=sa : supf1 a ≡ supf1 (supf1 a) -- supf0 a o≤ px
1216 ssa=sa = sym ( sup=u ? ? ? )
1217 sa<b : supf1 a o< b -- supf1 (supf1 a) ≡ supf1 a o< supf1 b → inject supf1 a o< b
1218 sa<b = supf-inject0 supf1-mono (subst (λ k → k o< supf1 b ) ? sa<sb )
1219 z20 : w ≤ supf1 b 1198 z20 : w ≤ supf1 b
1220 z20 with trio< b px 1199 z20 with trio< b px
1221 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) 1200 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb)
1222 (fcup fc (o<→≤ (ordtrans a<b b<px))) 1201 (fcup fc (o<→≤ (ordtrans a<b b<px)))
1223 ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where 1202 ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26 where
1224 -- sa<b : supf1 a o< b -- px
1225 -- sa<b = ?
1226 z26 : odef ( UnionCF A f ay supf0 b ) w 1203 z26 : odef ( UnionCF A f ay supf0 b ) w
1227 z26 with cfcs a<b b≤x sa<b fc 1204 z26 with x<y∨y≤x (supf1 a) b
1205 ... | case2 b≤sa = ?
1206 ... | case1 sa<b with cfcs a<b b≤x sa<b fc
1228 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 1207 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫
1229 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫ 1208 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫
1230 ... | tri> ¬a ¬b px<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) 1209 ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b
1231 -- sa<b : supf1 a o< b -- b ≡ x 1210 ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc)))
1232 -- sa<b = ? 1211 ... | case2 b≤sa = ? -- x=b x o≤ sa UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
1233 1212
1234 ... | no lim with trio< x o∅ 1213 ... | no lim with trio< x o∅
1235 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 1214 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
1236 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ? 1215 ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?
1237 ; supfmax = ? ; is-minsup = ? ; cfcs = ? } 1216 ; supfmax = ? ; is-minsup = ? ; cfcs = ? }