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

comparison src/zorn.agda @ 1036:23a8e4d558e0

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 15:49:50 +0900
parents 2144ef00cab9
children 23e185ef2737
comparison
equal deleted inserted replaced
1035:2144ef00cab9 1036:23a8e4d558e0
1026 zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 1026 zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
1027 zc21 {z1} (fsuc z2 fc ) with zc21 fc 1027 zc21 {z1} (fsuc z2 fc ) with zc21 fc
1028 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 1028 ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
1029 ... | case1 ⟪ ua1 , ch-is-sup u u<x su=u fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫ 1029 ... | case1 ⟪ ua1 , ch-is-sup u u<x su=u fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫
1030 ... | case2 fc = case2 (fsuc _ fc) 1030 ... | case2 fc = case2 (fsuc _ fc)
1031 zc21 (init asp refl ) = ? 1031 zc21 (init asp refl ) with trio< (supf0 u) (supf0 px)
1032 ... | tri< a ¬b ¬c = case1 ⟪ asp , ch-is-sup u u<px (trans (sym (sf1=sf0 (o<→≤ u<px))) su=u )(init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
1033 u<px : u o< px
1034 u<px = ZChain.supf-inject zc a
1035 asp0 : odef A (supf0 u)
1036 asp0 = ZChain.asupf zc
1037 ... | tri≈ ¬a b ¬c = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) )
1038 (sym (trans (sf1=sf0 (zc-b<x _ u<x)) b )))
1039 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
1032 1040
1033 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z) 1041 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
1034 is-minsup {z} z≤x with osuc-≡< z≤x 1042 is-minsup {z} z≤x with osuc-≡< z≤x
1035 ... | case1 z<x = ZChain.is-minsup zc (zc-b<x z<x) 1043 ... | case1 z=x = record { as = zc22 ; x≤sup = z23 ; minsup = z24 } where
1036 ... | case2 z=x = ? 1044 px<z : px o< z
1045 px<z = subst (λ k → px o< k) (sym z=x) px<x
1046 zc22 : odef A (supf1 z)
1047 zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z )) ( MinSUP.as sup1 )
1048 z26 : supf1 px ≤ supf1 x
1049 z26 = subst₂ (λ j k → j ≤ k ) (sym (sf1=sf0 o≤-refl )) (sym (sf1=sp1 px<x )) sfpx≤sp1
1050 z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
1051 z23 {w} uz with zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz )
1052 ... | case1 uz = ≤-ftrans z25 (subst₂ (λ j k → j ≤ supf1 k) (sf1=sf0 o≤-refl) (sym z=x) z26 ) where
1053 z25 : w ≤ supf0 px
1054 z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz
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 )
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
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
1061 z27 : supf1 px ≡ px --- sp1 o≤ x
1062 z27 = ?
1063 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
1065 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where
1066 u≤px : u o< osuc px
1067 u≤px = ordtrans u<x <-osuc
1068 u<z : u o< z
1069 u<z = ordtrans u<x (subst (λ k → px o< k ) (sym z=x) px<x )
1070 ... | case2 z<x = record { as = zc22 ; x≤sup = z23 ; minsup = z24 } where
1071 z≤px = zc-b<x _ z<x
1072 m = ZChain.is-minsup zc z≤px
1073 zc22 : odef A (supf1 z)
1074 zc22 = subst (λ k → odef A k ) (sym (sf1=sf0 z≤px)) ( IsMinSUP.as m )
1075 z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z
1076 z23 {w} ⟪ ua , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px)) ( ZChain.fcy<sup zc z≤px fc )
1077 z23 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px))
1078 (IsMinSUP.x≤sup m ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px )) su=u) (fcup fc u≤px ) ⟫ ) where
1079 u≤px : u o≤ px
1080 u≤px = ordtrans u<x z≤px
1081 z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s )
1082 → supf1 z o≤ s
1083 z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf0 z≤px)) ( IsMinSUP.minsup m as z25 ) where
1084 z25 : {w : Ordinal } → odef ( UnionCF A f ay supf0 z ) w → w ≤ s
1085 z25 {w} ⟪ ua , ch-init fc ⟫ = sup ⟪ ua , ch-init fc ⟫
1086 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = sup ⟪ ua , ch-is-sup u u<x
1087 (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where
1088 u≤px : u o≤ px
1089 u≤px = ordtrans u<x z≤px
1037 1090
1038 order : {a b : Ordinal} {w : Ordinal} → 1091 order : {a b : Ordinal} {w : Ordinal} →
1039 b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b 1092 b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b
1040 order {a} {b} {w} b≤x a<b fc with trio< b px 1093 order {a} {b} {w} b≤x a<b fc with trio< b px
1041 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) )) 1094 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) ))