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

comparison src/zorn.agda @ 956:a2b13a4b6727

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 Thu, 03 Nov 2022 12:11:38 +0900
parents bc27df170a1e
children ce42b1c5cf42
comparison
equal deleted inserted replaced
955:bc27df170a1e 956:a2b13a4b6727
477 m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ? 477 m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ?
478 m10 {s} as b-is-sup ⟪ aa , ch-is-sup u {w} u<x is-sup-z fc ⟫ = m01 where 478 m10 {s} as b-is-sup ⟪ aa , ch-is-sup u {w} u<x is-sup-z fc ⟫ = m01 where
479 m01 : w <= s 479 m01 : w <= s
480 m01 with trio< (supf u) (supf b) 480 m01 with trio< (supf u) (supf b)
481 ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ 481 ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫
482 ... | tri≈ ¬a b ¬c = <=-trans ? ( b-is-sup ⟪ aa , ch-is-sup u {w} ? is-sup-z fc ⟫ ) 482 ... | tri≈ ¬a b ¬c = ?
483 ... | tri> ¬a ¬b c = ? 483 ... | tri> ¬a ¬b c = ?
484 -- <=-trans (IsSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s 484 -- <=-trans (IsSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s
485 m07 : {s : Ordinal} → odef A s → ({z : Ordinal} → 485 m07 : {s : Ordinal} → odef A s → ({z : Ordinal} →
486 odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s 486 odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
487 m07 {s} as b-is-sup = IsSup.minsup is-sup as (m10 as b-is-sup ) 487 m07 {s} as b-is-sup = IsSup.minsup is-sup as (m10 as b-is-sup )
680 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f 680 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
681 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 681 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
682 chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) 682 chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } )
683 m05 : ZChain.supf zc b ≡ b 683 m05 : ZChain.supf zc b ≡ b
684 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) 684 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) )
685 ⟪ ? , m04 ⟫ where 685 ⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz)
686 m10 : {s : Ordinal } → (odef A s ) 686 ; minsup = m07 } , m04 ⟫ where
687 → ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) 687 m10 : {s : Ordinal } → (odef A s )
688 → {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s) 688 → ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) )
689 m10 = ? 689 → {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
690 m07 : {sup1 : Ordinal} → odef A sup1 → ({z : Ordinal} → 690 m10 = ?
691 odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ sup1) ∨ (z << sup1)) → b o≤ sup1 691 m07 : {s : Ordinal} → odef A s → ({z : Ordinal} →
692 m07 {s} as min = IsSup.minsup (proj2 is-sup) as (m10 as min) 692 odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
693 m07 {s} as s-is-sup = IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup)
693 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b 694 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
694 m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz 695 m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
695 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 696 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
696 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b 697 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
697 m09 {s} {z} s<b fcz = order b<A s<b fcz 698 m09 {s} {z} s<b fcz = order b<A s<b fcz