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

comparison src/zorn.agda @ 1026:8b3d7c461a84

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 Sat, 26 Nov 2022 07:51:09 +0900
parents e4919cc0cfe8
children 91988ae176ab
comparison
equal deleted inserted replaced
1025:e4919cc0cfe8 1026:8b3d7c461a84
1068 z50 : odef (UnionCF A f mf ay supf1 b) w 1068 z50 : odef (UnionCF A f mf ay supf1 b) w
1069 z50 with osuc-≡< px≤sa 1069 z50 with osuc-≡< px≤sa
1070 ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc) ⟫ where 1070 ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc) ⟫ where
1071 sa≤px : supf0 a o≤ px 1071 sa≤px : supf0 a o≤ px
1072 sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x 1072 sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
1073 spx=sa : supf0 px ≡ supf0 a
1074 spx=sa = begin
1075 supf0 px ≡⟨ cong supf0 px=sa ⟩
1076 supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩
1077 supf0 a ∎ where open ≡-Reasoning
1073 z51 : supf0 px o< b 1078 z51 : supf0 px o< b
1074 z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩ 1079 z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩
1075 supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩
1076 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 1080 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩
1077 supf1 a ∎ )) sa<b where open ≡-Reasoning 1081 supf1 a ∎ )) sa<b where open ≡-Reasoning
1078 z52 : supf1 a ≡ supf1 (supf0 px) 1082 z52 : supf1 a ≡ supf1 (supf0 px)
1079 z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 1083 z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩
1080 supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 1084 supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩
1081 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ 1085 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩
1082 supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ 1086 supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩
1083 supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa) ⟩
1084 supf1 (supf0 px) ∎ where open ≡-Reasoning 1087 supf1 (supf0 px) ∎ where open ≡-Reasoning
1085 m : MinSUP A (UnionCF A f mf ay supf0 px) 1088 m : MinSUP A (UnionCF A f mf ay supf0 px)
1086 m = ZChain.minsup zc o≤-refl 1089 m = ZChain.minsup zc o≤-refl
1087 m=spx : MinSUP.sup m ≡ supf1 (supf0 px) 1090 m=spx : MinSUP.sup m ≡ supf1 (supf0 px)
1088 m=spx = begin 1091 m=spx = begin
1089 MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl) ⟩ 1092 MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl) ⟩
1090 supf0 px ≡⟨ cong supf0 px=sa ⟩ 1093 supf0 px ≡⟨ cong supf0 px=sa ⟩
1091 supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ 1094 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩
1092 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 1095 supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩
1093 supf1 a ≡⟨ z52 ⟩
1094 supf1 (supf0 px) ∎ where open ≡-Reasoning 1096 supf1 (supf0 px) ∎ where open ≡-Reasoning
1095 z53 : supf1 (supf0 px) ≡ supf0 px 1097 z53 : supf1 (supf0 px) ≡ supf0 px
1096 z53 = begin 1098 z53 = begin
1097 supf1 (supf0 px) ≡⟨ sym z52 ⟩ 1099 supf1 (supf0 px) ≡⟨ cong supf1 spx=sa ⟩
1098 supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 1100 supf1 (supf0 a) ≡⟨ sf1=sf0 sa≤px ⟩
1099 supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩
1100 supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩ 1101 supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩
1101 supf0 px ∎ where open ≡-Reasoning 1102 supf0 px ∎ where open ≡-Reasoning
1102 cp : ChainP A f mf ay supf1 (supf0 px) 1103 cp : ChainP A f mf ay supf1 (supf0 px)
1103 cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ) 1104 cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ )
1104 ; order = order 1105 ; order = order
1105 ; supu=u = z53 } where 1106 ; supu=u = z53 } where
1106 uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 1107 uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
1107 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) 1108 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1)
1108 (sf1=sf0 (o<→≤ s<px)) fc ) where 1109 (sf1=sf0 (o<→≤ s<px)) fc ) where
1110 s<spx : s o< supf0 px
1111 s<spx = supf-inject0 supf1-mono ss<sp
1109 s<px : s o< px 1112 s<px : s o< px
1110 s<px = ZChain.supf-inject zc (osucprev ( begin 1113 s<px = osucprev ( begin
1111 osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩ 1114 osuc s ≤⟨ osucc s<spx ⟩
1112 osuc (supf1 s) ≤⟨ osucc ss<sp ⟩ 1115 supf0 px ≡⟨ spx=sa ⟩
1113 supf1 (supf0 px) ≡⟨ z53 ⟩ 1116 supf0 a ≡⟨ sym px=sa ⟩
1114 supf0 px ∎ )) where open o≤-Reasoning O 1117 px ∎ ) where open o≤-Reasoning O
1115 ss<px : supf0 s o< px 1118 ss<px : supf0 s o< px
1116 ss<px = osucprev ( begin 1119 ss<px = osucprev ( begin
1117 osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩ 1120 osuc (supf0 s) ≡⟨ cong osuc (sym (sf1=sf0 (o<→≤ s<px))) ⟩
1118 osuc (supf1 s) ≤⟨ osucc ss<sp ⟩ 1121 osuc (supf1 s) ≤⟨ osucc ss<sp ⟩
1119 supf1 (supf0 px) ≡⟨ sym z52 ⟩ 1122 supf1 (supf0 px) ≡⟨ sym z52 ⟩
1120 supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 1123 supf1 a ≡⟨ sf1=sf0 a≤px ⟩
1121 supf0 a ≡⟨ sym px=sa ⟩ 1124 supf0 a ≡⟨ sym px=sa ⟩
1122 px ∎ ) where open o≤-Reasoning O 1125 px ∎ ) where open o≤-Reasoning O