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

comparison src/zorn.agda @ 1076:7e047b46c3b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is-minsup done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 16 Dec 2022 09:03:29 +0900
parents 4e986bf9be8c
children faa512b2425c
comparison
equal deleted inserted replaced
1075:4e986bf9be8c 1076:7e047b46c3b2
1468 1468
1469 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z) 1469 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
1470 is-minsup {z} z≤x with osuc-≡< z≤x 1470 is-minsup {z} z≤x with osuc-≡< z≤x
1471 ... | case1 z=x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where 1471 ... | case1 z=x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where
1472 zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z 1472 zm00 : {w : Ordinal } → odef (UnionCF A f ay supf1 z) w → w ≤ supf1 z
1473 zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym ?) ( MinSUP.x≤sup usup ⟪ az , ic-init fc ⟫ ) 1473 zm00 {w} ⟪ az , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x))) ( MinSUP.x≤sup usup ⟪ az , ic-init fc ⟫ )
1474 zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym ? ) 1474 zm00 {w} ⟪ az , ch-is-sup u u<b su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=spu (sym z=x)))
1475 ( MinSUP.x≤sup usup ⟪ az , ic-isup u ? ? ? ⟫ ) 1475 ( MinSUP.x≤sup usup ⟪ az , ic-isup u u<x (o≤-refl0 zm05) (subst (λ k → FClosure A f k w) (sym zm06) fc) ⟫ ) where
1476 u<x : u o< x
1477 u<x = subst (λ k → u o< k) z=x u<b
1478 zm06 : supfz (subst (λ k → u o< k) z=x u<b) ≡ supf1 u
1479 zm06 = trans (zeq _ _ o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<x ))
1480 zm05 : supfz (subst (λ k → u o< k) z=x u<b) ≡ u
1481 zm05 = trans zm06 su=u
1476 zm01 : { s : Ordinal } → odef A s → ( {x : Ordinal } → odef (UnionCF A f ay supf1 z) x → x ≤ s ) → supf1 z o≤ s 1482 zm01 : { s : Ordinal } → odef A s → ( {x : Ordinal } → odef (UnionCF A f ay supf1 z) x → x ≤ s ) → supf1 z o≤ s
1477 zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=spu (sym z=x))) ( MinSUP.minsup usup as zm02 ) where 1483 zm01 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=spu (sym z=x))) ( MinSUP.minsup usup as zm02 ) where
1478 zm02 : {w : Ordinal } → odef pchainU w → w ≤ s 1484 zm02 : {w : Ordinal } → odef pchainU w → w ≤ s
1479 zm02 {w} ⟪ az , ic-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ 1485 zm02 {w} uw with pchainU⊆chain uw
1480 zm02 {w} ⟪ az , ic-isup u u<x sa<x fc ⟫ = sup ⟪ az , ch-is-sup u 1486 ... | ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫
1481 (subst (λ k → u o< k) (sym z=x) u<x) ? (subst (λ k → FClosure A f k w) (sym (sf1=sf u<x)) fc) ⟫ 1487 ... | ⟪ az , ch-is-sup u1 u<b su=u fc ⟫ = sup ⟪ az , ch-is-sup u1 (ordtrans u<b zm05) (trans zm03 su=u) zm04 ⟫ where
1482 -- with ZChain.cfcs (pzc (ob<x lim u<x)) <-osuc o≤-refl sa<x fc 1488 zm05 : osuc (IChain-i (proj2 uw)) o< z
1483 -- ... | ⟪ az , ch-init fc ⟫ = sup ⟪ az , ch-init fc ⟫ 1489 zm05 = subst (λ k → osuc (IChain-i (proj2 uw)) o< k) (sym z=x) ( pic<x (proj2 uw) )
1484 -- ... | ⟪ az , ch-is-sup u1 u<b su=u fc ⟫ = sup ⟪ az , ch-is-sup u1 (ordtrans u<b ?) ? (subst (λ k → FClosure A f k w) (sym (sf1=sf ?)) ? ) ⟫ 1490 u<x : u1 o< x
1491 u<x = subst (λ k → u1 o< k) z=x ( ordtrans u<b zm05 )
1492 zm03 : supf1 u1 ≡ ZChain.supf (prev (osuc (IChain-i (proj2 uw))) (pic<x (proj2 uw))) u1
1493 zm03 = trans (sf1=sf u<x) (zeq _ _ (osucc u<b) (o<→≤ <-osuc) )
1494 zm04 : FClosure A f (supf1 u1) w
1495 zm04 = subst (λ k → FClosure A f k w) (sym zm03) fc
1485 ... | case2 z<x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where 1496 ... | case2 z<x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where
1486 supf0 = ZChain.supf (pzc (ob<x lim z<x)) 1497 supf0 = ZChain.supf (pzc (ob<x lim z<x))
1487 msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z) 1498 msup : IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)
1488 msup = ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) 1499 msup = ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc)
1489 s1=0 : {u : Ordinal } → u o< z → supf1 u ≡ supf0 u 1500 s1=0 : {u : Ordinal } → u o< z → supf1 u ≡ supf0 u