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

comparison src/zorn.agda @ 971:4fdf889ca95a

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 Mon, 07 Nov 2022 10:23:53 +0900
parents 980bc43ca6c1
children 520aff512969
comparison
equal deleted inserted replaced
970:980bc43ca6c1 971:4fdf889ca95a
881 -- supf px < px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x 881 -- supf px < px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
882 -- supf px ≡ px → UnionCF A f mf ay supf px ⊂ UnionCF A f mf ay supf x ≡ pchainx 882 -- supf px ≡ px → UnionCF A f mf ay supf px ⊂ UnionCF A f mf ay supf x ≡ pchainx
883 -- x < supf px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x 883 -- x < supf px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
884 884
885 zc43 : ( x o< sp1 ) ∨ ( sp1 o≤ x ) 885 zc43 : ( x o< sp1 ) ∨ ( sp1 o≤ x )
886 zc43 = ? 886 zc43 with trio< x sp1
887 ... | tri< a ¬b ¬c = case1 a
888 ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
889 ... | tri> ¬a ¬b c = case2 (o<→≤ c)
887 890
888 zc41 : ZChain A f mf ay x 891 zc41 : ZChain A f mf ay x
889 zc41 with zc43 892 zc41 with zc43
890 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? 893 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
891 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where 894 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where
1040 ... | tri< a ¬b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) 1043 ... | tri< a ¬b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x))
1041 (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) ( o<→≤ a ) 1044 (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) ( o<→≤ a )
1042 ... | tri≈ ¬a b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x)) 1045 ... | tri≈ ¬a b ¬c = subst₂ ( λ j k → j o≤ k) (sym (sf1=sp1 px<x))
1043 (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) (o≤-refl0 b) 1046 (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) (o≤-refl0 b)
1044 ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 )) 1047 ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 ))
1048
1049 3cases : (¬ (supf0 px ≡ px)) ∨ ( ¬ (supf0 px o< sp1 )) ∨ ( (supf0 px ≡ px) ∧ (supf0 px o< sp1 ))
1050 3cases with o≡? (supf0 px) px
1051 ... | no ne = case1 ne
1052 ... | yes eq with trio< (supf0 px) sp1
1053 ... | tri< a ¬b ¬c = case2 (case2 ⟪ eq , a ⟫ )
1054 ... | tri≈ ¬a b ¬c = case2 (case1 ¬a )
1055 ... | tri> ¬a ¬b c = case2 (case1 ¬a )
1045 1056
1046 zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z 1057 zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
1047 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ 1058 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
1048 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where 1059 zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
1049 u<px : u o< px 1060 u<px : u o< px
1162 -- z1 o< px → supf1 z1 ≡ supf0 z1 1173 -- z1 o< px → supf1 z1 ≡ supf0 z1
1163 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 1174 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1
1164 -- z1 ≡ px , supf0 px ≡ px 1175 -- z1 ≡ px , supf0 px ≡ px
1165 psz1≤px : supf1 z1 o≤ px 1176 psz1≤px : supf1 z1 o≤ px
1166 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x 1177 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x
1167 sf0px<sp1 : supf0 px o< sp1 -- px o< sp1 o≤ x .. sp1 ≡ x
1168 sf0px<sp1 = ?
1169 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1178 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1170 csupf2 with trio< z1 px | inspect supf1 z1 1179 csupf2 with 3cases
1171 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px 1180 ... | case2 (case2 p) with trio< z1 px | inspect supf1 z1
1172 ... | case2 lt = zc12 ? ? (case1 cs03) where 1181 ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
1182 ... | case2 lt = zc12 (proj1 p) (proj2 p) (case1 cs03) where
1173 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) 1183 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
1174 cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) 1184 cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
1175 ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) 1185 ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) )
1176 ... | case1 sfz=sfpx = zc12 ? ? (case2 (init (ZChain.asupf zc) cs04 )) where 1186 ... | case1 sfz=sfpx = zc12 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where
1177 supu=u : supf1 (supf1 z1) ≡ supf1 z1
1178 supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx)
1179 cs04 : supf0 px ≡ supf0 z1 1187 cs04 : supf0 px ≡ supf0 z1
1180 cs04 = begin 1188 cs04 = begin
1181 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ 1189 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩
1182 supf1 px ≡⟨ sym sfz=sfpx ⟩ 1190 supf1 px ≡⟨ sym sfz=sfpx ⟩
1183 supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ 1191 supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩
1185 ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where 1193 ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where
1186 --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x 1194 --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x
1187 cs05 : px o< supf0 px 1195 cs05 : px o< supf0 px
1188 cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx 1196 cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
1189 cs06 : supf0 px o< osuc px 1197 cs06 : supf0 px o< osuc px
1190 cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ? 1198 cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x
1191 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 ? ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) 1199 csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (proj1 p) (proj2 p)
1192 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? 1200 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
1193 -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) 1201 csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where
1202 cs08 : px o< sp1
1203 cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p )
1204 cs09 : sp1 o< osuc px
1205 cs09 = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x
1206
1207 csupf2 | case2 (case1 p) = ?
1208 csupf2 | case1 p = ?
1194 1209
1195 1210
1196 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? 1211 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
1197 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where 1212 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where
1198 1213