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

comparison src/zorn.agda @ 968:9a8041a7f3c9

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 Sun, 06 Nov 2022 13:39:45 +0900
parents cd0ef83189c5
children ec7f3473ff55
comparison
equal deleted inserted replaced
967:cd0ef83189c5 968:9a8041a7f3c9
882 882
883 zc43 : ( x o< sp1 ) ∨ ( sp1 o≤ x ) 883 zc43 : ( x o< sp1 ) ∨ ( sp1 o≤ x )
884 zc43 = ? 884 zc43 = ?
885 885
886 zc41 : ZChain A f mf ay x 886 zc41 : ZChain A f mf ay x
887 zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) 887 zc41 with zc43
888 zc41 | (case2 sfpx<sp1) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? 888 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
889 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where 889 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where
890 -- supf0 px is included by the chain of sp1 890 -- supf0 px is included by the chain of sp1
891 -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 891 -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
892 -- supf1 x ≡ sp1, which is not included now 892 -- supf1 x ≡ sp1, which is not included now
893 893
906 sf1=sp1 : {z : Ordinal } → px o< z → supf1 z ≡ sp1 906 sf1=sp1 : {z : Ordinal } → px o< z → supf1 z ≡ sp1
907 sf1=sp1 {z} px<z with trio< z px 907 sf1=sp1 {z} px<z with trio< z px
908 ... | tri< a ¬b ¬c = ⊥-elim ( o<> px<z a ) 908 ... | tri< a ¬b ¬c = ⊥-elim ( o<> px<z a )
909 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) px<z ) 909 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) px<z )
910 ... | tri> ¬a ¬b c = refl 910 ... | tri> ¬a ¬b c = refl
911
912 sf=eq : { z : Ordinal } → z o< x → supf0 z ≡ supf1 z
913 sf=eq {z} z<x = sym (sf1=sf0 (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ))
911 914
912 asupf1 : {z : Ordinal } → odef A (supf1 z) 915 asupf1 : {z : Ordinal } → odef A (supf1 z)
913 asupf1 {z} with trio< z px 916 asupf1 {z} with trio< z px
914 ... | tri< a ¬b ¬c = ZChain.asupf zc 917 ... | tri< a ¬b ¬c = ZChain.asupf zc
915 ... | tri≈ ¬a b ¬c = ZChain.asupf zc 918 ... | tri≈ ¬a b ¬c = ZChain.asupf zc
936 zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) ) 939 zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) )
937 zc18 : supf0 a o≤ sp1 940 zc18 : supf0 a o≤ sp1
938 zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) 941 zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
939 ... | tri> ¬a ¬b c = o≤-refl 942 ... | tri> ¬a ¬b c = o≤-refl
940 943
944 sf≤ : { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
945 sf≤ {z} x≤z with trio< z px
946 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
947 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
948 ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c)
949 (supf1-mono (o<→≤ c ))
950 -- px o<z → spuf0 x ≡ supf0 px ≡ supf1 px o≤ supf1 z
941 951
942 fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z 952 fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z
943 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc 953 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
944 fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z 954 fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z
945 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc 955 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
1120 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) 1130 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
1121 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? 1131 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ?
1122 -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) 1132 -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
1123 1133
1124 1134
1125 zc41 | (case1 sfp=sp1 ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? 1135 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
1126 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where 1136 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where
1127 1137
1128 -- supf0 px not is included by the chain 1138 -- supf0 px not is included by the chain
1129 -- supf1 x ≡ supf0 px because of supfmax 1139 -- supf1 x ≡ supf0 px because of supfmax
1130 1140
1131 supf1 : Ordinal → Ordinal 1141 supf1 : Ordinal → Ordinal
1132 supf1 z with trio< z px 1142 supf1 z with trio< z px
1133 ... | tri< a ¬b ¬c = supf0 z 1143 ... | tri< a ¬b ¬c = supf0 z
1134 ... | tri≈ ¬a b ¬c = supf0 px 1144 ... | tri≈ ¬a b ¬c = supf0 z
1135 ... | tri> ¬a ¬b c = supf0 px 1145 ... | tri> ¬a ¬b c = supf0 px
1136 1146
1137 sf1=sf0 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z 1147 sf1=sf0 : {z : Ordinal } → z o< px → supf1 z ≡ supf0 z
1138 sf1=sf0 {z} z<px with trio< z px 1148 sf1=sf0 {z} z<px with trio< z px
1139 ... | tri< a ¬b ¬c = refl 1149 ... | tri< a ¬b ¬c = refl
1140 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px ) 1150 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<px )
1141 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px ) 1151 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<px )
1152
1153 sf=eq : { z : Ordinal } → z o< x → supf0 z ≡ supf1 z
1154 sf=eq {z} z<x with trio< z px
1155 ... | tri< a ¬b ¬c = refl
1156 ... | tri≈ ¬a b ¬c = refl
1157 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op)) z<x ⟫ )
1158 sf≤ : { z : Ordinal } → x o≤ z → supf0 x o≤ supf1 z
1159 sf≤ {z} x≤z with trio< z px
1160 ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) )
1161 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
1162 ... | tri> ¬a ¬b c = o≤-refl0 ( ZChain.supfmax zc px<x )
1142 1163
1143 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px 1164 zc17 : {z : Ordinal } → supf0 z o≤ supf0 px
1144 zc17 = ? -- px o< z, px o< supf0 px 1165 zc17 = ? -- px o< z, px o< supf0 px
1145 1166
1146 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w 1167 supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w
1150 ... | tri< a ¬b ¬c = zc17 1171 ... | tri< a ¬b ¬c = zc17
1151 ... | tri≈ ¬a refl ¬c = o≤-refl 1172 ... | tri≈ ¬a refl ¬c = o≤-refl
1152 ... | tri> ¬a ¬b c = o≤-refl 1173 ... | tri> ¬a ¬b c = o≤-refl
1153 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px 1174 supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px
1154 ... | tri< a ¬b ¬c = zc17 1175 ... | tri< a ¬b ¬c = zc17
1155 ... | tri≈ ¬a b ¬c = o≤-refl 1176 ... | tri≈ ¬a b ¬c = o≤-refl0 ?
1156 ... | tri> ¬a ¬b c = o≤-refl 1177 ... | tri> ¬a ¬b c = o≤-refl
1157 1178
1158 pchain1 : HOD 1179 pchain1 : HOD
1159 pchain1 = UnionCF A f mf ay supf1 x 1180 pchain1 = UnionCF A f mf ay supf1 x
1160 1181