Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 905:e6a282eb12fe
union equal passed
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Oct 2022 12:20:38 +0900 |
| parents | 4541c9974e53 |
| children | 02f250be89e2 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 45 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 10 09:33:54 2022 +0900 +++ b/src/zorn.agda Mon Oct 10 12:20:38 2022 +0900 @@ -448,18 +448,7 @@ -- ordering is not proved here but in ZChain1 - supf-idem : {x : Ordinal } → supf x o≤ z - → ¬ HasPrev A (UnionCF A f mf ay supf (supf x)) (supf x) f - → supf (supf x) ≡ supf x - supf-idem {x} sx≤z ¬np = sup=u asupf sx≤z ⟪ record { x<sup = si00 } , ¬np ⟫ where - ms : MinSUP A (UnionCF A f mf ay supf (supf x)) - ms = minsup sx≤z - mseq : supf (supf x) ≡ MinSUP.sup ( minsup sx≤z ) - mseq = supf-is-minsup sx≤z - si00 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf x)) w → (w ≡ supf x) ∨ (w << supf x) - si00 {w} uw with MinSUP.x<sup ms uw - ... | case1 eq = case1 (subst (λ k → w ≡ k ) ? eq) - ... | case2 lt = case2 (subst (λ k → w << k ) ? lt) + -- supf-idem : {x : Ordinal } → supf x o< z → supf (supf x) ≡ supf x record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where @@ -1005,32 +994,50 @@ zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ - zc21 (init asp refl ) = ⟪ asp , ch-is-sup (supf0 px) sfpx<x - record {fcy<sup = ? ; order = zc18 ; supu=u = zc15 } (init (asupf1 {supf0 px}) zc15) ⟫ where - zc15 : supf1 (supf0 px) ≡ supf0 px - zc15 = ? - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) - zc18 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px)) - zc18 {s} {z1} ss<sf fc = ? - zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx - (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where - mins : MinSUP A (UnionCF A f mf ay supf0 px) - mins = ZChain.minsup zc o≤-refl - mins-is-spx : MinSUP.sup mins ≡ supf1 px - mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl )) - s<px : s o< px - s<px = supf-inject0 supf1-mono ss<spx - sf≤px : supf0 s o≤ px - sf≤px = subst (λ k → supf0 s o< k ) ? (ordtrans ? sfpx<x ) - csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 - csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) - csupf17 (init as refl ) with osuc-≡< sf≤px - ... | case2 sf<px = ZChain.csupf zc sf<px - ... | case1 sf=px = ? + zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x ) + ... | case1 sfpx=px = ⟪ asp , ch-is-sup px (pxo<x op) + record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where + zc15 : supf1 px ≡ px + zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) + zc14 : FClosure A f (supf1 px) (supf0 px) + zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl) + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) + zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx + (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where + mins : MinSUP A (UnionCF A f mf ay supf0 px) + mins = ZChain.minsup zc o≤-refl + mins-is-spx : MinSUP.sup mins ≡ supf1 px + mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl )) + s<px : s o< px + s<px = supf-inject0 supf1-mono ss<spx + sf<px : supf0 s o< px + sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx + csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 + csupf17 (init as refl ) = ZChain.csupf zc sf<px + csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) + + ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) + ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) + record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫ where + z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) + z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) (ChainP.fcy<sup is-sup fc) + z11 : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1 + → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u ) + z11 {s} {z} lt fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) + (ChainP.order is-sup lt0 (fcup fc s≤px )) where + s<u : s o< u + s<u = supf-inject0 supf1-mono lt + s≤px : s o≤ px + s≤px = ordtrans s<u (o<→≤ u≤x) + lt0 : supf0 s o< supf0 u + lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u≤x)) lt + z12 : supf1 u ≡ u + z12 = trans (sf1=sf0 (o<→≤ u≤x)) (ChainP.supu=u is-sup) + record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where