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

comparison src/zorn.agda @ 1006:ac182ad5bfd2

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, 19 Nov 2022 00:04:35 +0900
parents 2808471040c0
children 88fae58f89f5
comparison
equal deleted inserted replaced
1005:2808471040c0 1006:ac182ad5bfd2
509 im00 : f (f pr) <= sp 509 im00 : f (f pr) <= sp
510 im00 = is-sup ( f-next (f-next (HasPrev.ay hp))) 510 im00 = is-sup ( f-next (f-next (HasPrev.ay hp)))
511 fsp≤sp : f sp <= sp 511 fsp≤sp : f sp <= sp
512 fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00 512 fsp≤sp = subst (λ k → f k <= sp ) (sym (HasPrev.x=fy hp)) im00
513 513
514 csupf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o< z → supf (supf b) ≡ supf b 514 supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b
515 csupf-idem mf< {b} b≤z sfb<x = z52 where 515 supf-idem mf< {b} b≤z sfb≤x = z52 where
516 z54 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) 516 z54 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
517 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc 517 z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
518 z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k )) 518 z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k ))
519 (sym (supf-is-minsup b≤z)) 519 (sym (supf-is-minsup b≤z))
520 (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z su<z fc )) where 520 (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z su<z fc )) where
521 u<b : u o< b 521 u<b : u o< b
522 u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x ) 522 u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x )
523 su<z : supf u o< z 523 su<z : supf u o< z
524 su<z = subst (λ k → k o< z ) (sym (ChainP.supu=u is-sup)) ( ordtrans<-≤ u<b b≤z ) 524 su<z = subst (λ k → k o< z ) (sym (ChainP.supu=u is-sup)) ( ordtrans<-≤ u<b b≤z )
525 z52 : supf (supf b) ≡ supf b 525 z52 : supf (supf b) ≡ supf b
526 z52 = sup=u asupf (o<→≤ sfb<x) ⟪ record { x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 526 z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
527 527
528 UChain⊆ : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 528 UChain⊆ : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
529 {z y : Ordinal} (ay : odef A y) { supf supf1 : Ordinal → Ordinal } 529 {z y : Ordinal} (ay : odef A y) { supf supf1 : Ordinal → Ordinal }
530 → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) 530 → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y )
531 → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x) 531 → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x)
1064 csupf1 with trio< (supf0 px) x 1064 csupf1 with trio< (supf0 px) x
1065 ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫ where 1065 ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫ where
1066 spx = supf0 px 1066 spx = supf0 px
1067 spx≤px : supf0 px o≤ px 1067 spx≤px : supf0 px o≤ px
1068 spx≤px = zc-b<x _ sfpx<x 1068 spx≤px = zc-b<x _ sfpx<x
1069 z54 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (supf0 px)) z → (z ≡ supf0 px) ∨ (z << supf0 px)
1070 z54 {z} ⟪ az , ch-init fc ⟫ = ZChain.fcy<sup zc o≤-refl fc
1071 z54 {z} ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = subst (λ k → (z ≡ k) ∨ (z << k ))
1072 (sym (ZChain.supf-is-minsup zc o≤-refl))
1073 (MinSUP.x≤sup (ZChain.minsup zc o≤-refl) (ZChain.cfcs zc mf< u<px o≤-refl ? fc )) where
1074 u<px : u o< px
1075 u<px = ZChain.supf-inject zc ( subst (λ k → k o< supf0 px) (sym (ChainP.supu=u is-sup)) u<b )
1076 -- u<b : u o< supf0 px
1077 -- is-sup : ChainP A f mf ay (ZChain.supf zc) u
1078 -- fc : FClosure A f (ZChain.supf zc u) z
1079 z52 : supf1 (supf0 px) ≡ supf0 px 1069 z52 : supf1 (supf0 px) ≡ supf0 px
1080 z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.sup=u zc (ZChain.asupf zc) (zc-b<x _ sfpx<x) 1070 z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl ? )
1081 ⟪ record { x≤sup = z54 } , ZChain.IsMinSUP→NotHasPrev zc (ZChain.asupf zc) z54 (( λ ax → proj1 (mf< _ ax))) ⟫ )
1082 fc1 : FClosure A f (supf1 spx) w 1071 fc1 : FClosure A f (supf1 spx) w
1083 fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc 1072 fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
1084 order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx) 1073 order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx)
1085 order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) 1074 order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k ))
1086 (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) ) 1075 (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) )