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

comparison src/zorn.agda @ 997:908369b2d08b

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 Thu, 17 Nov 2022 17:04:47 +0900
parents 61d74b3d5456
children e5f46d08c074
comparison
equal deleted inserted replaced
996:61d74b3d5456 997:908369b2d08b
1031 1031
1032 fcs<sup : {a b w : Ordinal } → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w 1032 fcs<sup : {a b w : Ordinal } → a o< b → b o≤ x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
1033 fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px 1033 fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px
1034 ... | tri< a<px ¬b ¬c = z50 where 1034 ... | tri< a<px ¬b ¬c = z50 where
1035 z50 : odef (UnionCF A f mf ay supf1 b) w 1035 z50 : odef (UnionCF A f mf ay supf1 b) w
1036 z50 with ZChain.fcs<sup zc a<px o≤-refl fc 1036 z50 with osuc-≡< b≤x
1037 ... | case2 lt with ZChain.fcs<sup zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) fc
1037 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 1038 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
1038 ... | ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u ? ? ? ⟫ 1039 ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px ) ⟫ where -- u o< px → u o< b ?
1039 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b ? ? ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x 1040 u≤px : u o≤ px
1041 u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ u<b b≤x )
1042 u<x : u o< x
1043 u<x = ordtrans<-≤ u<b b≤x
1044 cp1 : ChainP A f mf ay supf1 u
1045 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc )
1046 ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x)
1047 (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) ))
1048 (sym (sf=eq u<x)) s<u)
1049 (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
1050 ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup) }
1051 z50 | case1 eq with ZChain.fcs<sup zc a<px o≤-refl fc
1052 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
1053 ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫ where -- u o< px → u o< b ?
1054 u<b : u o< b
1055 u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc )
1056 u<x : u o< x
1057 u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc )
1058 cp1 : ChainP A f mf ay supf1 u
1059 cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc )
1060 ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x)
1061 (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) ))
1062 (sym (sf=eq u<x)) s<u)
1063 (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
1064 ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup) }
1065 ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b cp1 z51 ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x
1040 px<b : px o< b 1066 px<b : px o< b
1041 px<b = subst₂ (λ j k → j o< k) a=px refl a<b 1067 px<b = subst₂ (λ j k → j o< k) a=px refl a<b
1042 b=x : b ≡ x 1068 b=x : b ≡ x
1043 b=x with trio< b x 1069 b=x with trio< b x
1044 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) -- px o< b o< x 1070 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) -- px o< b o< x
1045 ... | tri≈ ¬a b ¬c = b 1071 ... | tri≈ ¬a b ¬c = b
1046 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b 1072 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b
1073 z51 : FClosure A f (supf1 px) w
1074 z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
1075 cp1 : ChainP A f mf ay supf1 px
1076 cp1 = record { fcy<sup = λ {z} fc → ?
1077 ; order = λ {s} {z} s<u fc → ?
1078 ; supu=u = ? }
1047 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x 1079 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x
1048 1080
1049 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z 1081 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
1050 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 1082 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
1051 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where 1083 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where
1086 m = ZChain.minsup zc (o<→≤ a) 1118 m = ZChain.minsup zc (o<→≤ a)
1087 ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) 1119 ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
1088 ms00 {x} ux = MinSUP.x≤sup m ? 1120 ms00 {x} ux = MinSUP.x≤sup m ?
1089 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → 1121 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
1090 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 1122 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
1091 ms01 {sup2} us P = MinSUP.minsup m ? ? 1123 ms01 {sup2} us P = MinSUP.minsup m us ?
1092 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m 1124 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m
1093 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where 1125 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where
1094 m = ZChain.minsup zc (o≤-refl0 b) 1126 m = ZChain.minsup zc (o≤-refl0 b)
1095 ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) 1127 ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
1096 ms00 {x} ux = MinSUP.x≤sup m ? 1128 ms00 {x} ux = MinSUP.x≤sup m ?
1097 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → 1129 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
1098 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 1130 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
1099 ms01 {sup2} us P = MinSUP.minsup m ? ? 1131 ms01 {sup2} us P = MinSUP.minsup m us ?
1100 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 1132 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
1101 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where 1133 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
1102 m = sup1 1134 m = sup1
1103 ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) 1135 ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
1104 ms00 {x} ux = MinSUP.x≤sup m ? 1136 ms00 {x} ux = MinSUP.x≤sup m ?
1105 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → 1137 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
1106 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 1138 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
1107 ms01 {sup2} us P = MinSUP.minsup m ? ? 1139 ms01 {sup2} us P = MinSUP.minsup m us ?
1108 1140
1109 1141
1110 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? 1142 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
1111 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; fcs<sup = ? } where 1143 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; fcs<sup = ? } where
1112 1144