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

comparison src/zorn.agda @ 1055:60211e5b1fe5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
order (px case) done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 09 Dec 2022 23:27:05 +0900
parents 38148b08d85c
children 0dff7ab7a55f
comparison
equal deleted inserted replaced
1054:38148b08d85c 1055:60211e5b1fe5
1251 ... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x 1251 ... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x
1252 ( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px))) sa<sb) )) 1252 ( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px))) sa<sb) ))
1253 (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 (o≤-refl0 b=px))) ))) where 1253 (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 (o≤-refl0 b=px))) ))) where
1254 x≤sa : x o≤ supf1 a 1254 x≤sa : x o≤ supf1 a
1255 x≤sa = subst (λ k → k o≤ supf1 a ) (trans (cong osuc b=px) (Oprev.oprev=x op)) (osucc b<sa ) 1255 x≤sa = subst (λ k → k o≤ supf1 a ) (trans (cong osuc b=px) (Oprev.oprev=x op)) (osucc b<sa )
1256 ... | case1 b=sa = z28 where 1256 ... | case1 b=sa = ⊥-elim (o<¬≡ sa=sb sa<sb) where
1257 a<x : a o< x 1257 sa=sb : supf1 a ≡ supf0 b
1258 a<x = ? 1258 sa=sb = begin
1259 z28 : odef (UnionCF A f ay supf0 b) w 1259 supf1 a ≡⟨ sf1=sf0 a≤px ⟩
1260 z28 with cfcs a<x ? ? fc 1260 supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px (o≤-refl0 (sym (trans (sym b=px) (trans b=sa (sf1=sf0 a≤px) ))))) ⟩
1261 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 1261 supf0 (supf0 a) ≡⟨ cong supf0 (sym (sf1=sf0 a≤px )) ⟩
1262 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? (fcup fc ?) ⟫ 1262 supf0 (supf1 a) ≡⟨ cong supf0 (sym b=sa) ⟩
1263 -- px ≡ supf1 a 1263 supf0 b ∎ where open ≡-Reasoning
1264 ... | case1 sa<b with cfcs a<b b≤x sa<b fc 1264 ... | case1 sa<b with cfcs a<b b≤x sa<b fc
1265 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 1265 ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫
1266 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px)) su=u) (fcup fc u≤px) ⟫ where 1266 ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px)) su=u) (fcup fc u≤px) ⟫ where
1267 u≤px : u o≤ px 1267 u≤px : u o≤ px
1268 u≤px = o<→≤ ( subst (λ k → u o< k ) b=px u<x ) 1268 u≤px = o<→≤ ( subst (λ k → u o< k ) b=px u<x )