Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 885:d1a850b5d8e4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Oct 2022 16:13:32 +0900 |
| parents | 36a50c66a00d |
| children | 7c4b65fcba97 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 62 insertions(+), 42 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Oct 02 10:19:31 2022 +0900 +++ b/src/zorn.agda Sun Oct 02 16:13:32 2022 +0900 @@ -906,48 +906,6 @@ ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b)) ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c ) - ch1x=pchainpx : UnionCF A f mf ay supf1 x ≡ pchainpx - ch1x=pchainpx = ==→o≡ record { eq→ = zc11 ; eq← = zc12 } where - fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z - fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (zc16 u≤px) fc - fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z - fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (zc16 u≤px)) fc - zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z - zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with trio< u px - ... | tri< a ¬b ¬c = case1 ⟪ az , ch-is-sup u a record {fcy<sup = zc13 ; order = ? ; supu=u = trans (sym (zc16 (o<→≤ a))) (ChainP.supu=u is-sup) } fc ⟫ where - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (zc16 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c = case2 fc - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x ⟫ ) - zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z - zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ - zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = ⟪ az , ch-is-sup u - (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc )) - record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 (o<→≤ u<x)) (ChainP.supu=u is-sup) } (fcpu fc (o<→≤ u<x)) ⟫ where - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc ) - zc12 {z} (case2 fc) = ⟪ A∋fc px f mf fc , ch-is-sup px (pxo<x op) record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 o≤-refl ) (sym sfpx=px) } - (subst (λ k → FClosure A f k z ) (trans sfpx=px (sym (zc16 o≤-refl ))) fc) ⟫ where - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) - - record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where - field - tsup : MinSUP A (UnionCF A f mf ay supf1 z) - tsup=sup : supf1 z ≡ MinSUP.sup tsup - - sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x - sup {z} z≤x with trio< z px - ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m - ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a)) } where - m = ZChain.minsup zc (o<→≤ a) - ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m - ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where - m = ZChain.minsup zc (o≤-refl0 b) - ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 - ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } - supf-mono1 : {z w : Ordinal } → z o≤ w → supf1 z o≤ supf1 w supf-mono1 {z} {w} z≤w with trio< w px ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (zc16 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w ) @@ -1020,6 +978,68 @@ zc23 eq = ⊥-elim (o<¬≡ eq sz0<sz1 ) ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl sz0<sz1 ) + ch1x=pchainpx : UnionCF A f mf ay supf1 x ≡ pchainpx + ch1x=pchainpx = ==→o≡ record { eq→ = zc11 ; eq← = zc12 } where + fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z + fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (zc16 u≤px) fc + fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z + fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (zc16 u≤px)) fc + zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z + zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ + zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc21 fc where + zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 + zc21 {z1} (fsuc z2 fc ) with zc21 fc + ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ + ... | case1 ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ + ... | case2 fc = case2 ? + zc21 (init asp refl ) with trio< u px | inspect supf1 u + ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = ? ; supu=u = trans (sym (zc16 (o<→≤ a))) (ChainP.supu=u is-sup) } ? ⟫ where + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (zc16 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = case2 ? + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x ⟫ ) + zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z + zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ + zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where + zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1 + 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 ) with trio< u px | inspect supf1 u + ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u + (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc )) + record {fcy<sup = zc13 ; order = ? ; supu=u = trans ? (ChainP.supu=u is-sup) } ? ⟫ where + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = ? + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? ⟫ ) + + zc12 {z} (case2 fc) = zc21 fc where + zc21 : {z1 : Ordinal } → FClosure A f px z1 → odef (UnionCF A f mf ay supf1 x) z1 + 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 px (pxo<x op) + record {fcy<sup = zc13 ; order = ? ; supu=u = trans (zc16 o≤-refl ) (sym sfpx=px) } (init ? ? ) ⟫ where + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (zc16 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) + + record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where + field + tsup : MinSUP A (UnionCF A f mf ay supf1 z) + tsup=sup : supf1 z ≡ MinSUP.sup tsup + + sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x + sup {z} z≤x with trio< z px + ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a)) } where + m = ZChain.minsup zc (o<→≤ a) + ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (zc16 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where + m = ZChain.minsup zc (o≤-refl0 b) + ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 + ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } + csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z