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

comparison src/zorn.agda @ 905:e6a282eb12fe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
904:4541c9974e53 905:e6a282eb12fe
446 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) 446 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) ))
447 ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) 447 ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
448 448
449 -- ordering is not proved here but in ZChain1 449 -- ordering is not proved here but in ZChain1
450 450
451 supf-idem : {x : Ordinal } → supf x o≤ z 451 -- supf-idem : {x : Ordinal } → supf x o< z → supf (supf x) ≡ supf x
452 → ¬ HasPrev A (UnionCF A f mf ay supf (supf x)) (supf x) f
453 → supf (supf x) ≡ supf x
454 supf-idem {x} sx≤z ¬np = sup=u asupf sx≤z ⟪ record { x<sup = si00 } , ¬np ⟫ where
455 ms : MinSUP A (UnionCF A f mf ay supf (supf x))
456 ms = minsup sx≤z
457 mseq : supf (supf x) ≡ MinSUP.sup ( minsup sx≤z )
458 mseq = supf-is-minsup sx≤z
459 si00 : {w : Ordinal} → odef (UnionCF A f mf ay supf (supf x)) w → (w ≡ supf x) ∨ (w << supf x)
460 si00 {w} uw with MinSUP.x<sup ms uw
461 ... | case1 eq = case1 (subst (λ k → w ≡ k ) ? eq)
462 ... | case2 lt = case2 (subst (λ k → w << k ) ? lt)
463 452
464 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 453 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
465 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 454 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
466 supf = ZChain.supf zc 455 supf = ZChain.supf zc
467 field 456 field
1003 zc12 {z} (case2 fc) = zc21 fc where 992 zc12 {z} (case2 fc) = zc21 fc where
1004 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 993 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
1005 zc21 {z1} (fsuc z2 fc ) with zc21 fc 994 zc21 {z1} (fsuc z2 fc ) with zc21 fc
1006 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 995 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
1007 ... | ⟪ 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₁) ⟫ 996 ... | ⟪ 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₁) ⟫
1008 zc21 (init asp refl ) = ⟪ asp , ch-is-sup (supf0 px) sfpx<x 997 zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x )
1009 record {fcy<sup = ? ; order = zc18 ; supu=u = zc15 } (init (asupf1 {supf0 px}) zc15) ⟫ where 998 ... | case1 sfpx=px = ⟪ asp , ch-is-sup px (pxo<x op)
1010 zc15 : supf1 (supf0 px) ≡ supf0 px 999 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
1011 zc15 = ? 1000 zc15 : supf1 px ≡ px
1012 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) 1001 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
1013 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) 1002 zc14 : FClosure A f (supf1 px) (supf0 px)
1014 zc18 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) → 1003 zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl)
1015 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px)) 1004 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
1016 zc18 {s} {z1} ss<sf fc = ? 1005 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
1017 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → 1006 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
1018 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) 1007 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
1019 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 1008 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx
1020 (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where 1009 (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
1021 mins : MinSUP A (UnionCF A f mf ay supf0 px) 1010 mins : MinSUP A (UnionCF A f mf ay supf0 px)
1022 mins = ZChain.minsup zc o≤-refl 1011 mins = ZChain.minsup zc o≤-refl
1023 mins-is-spx : MinSUP.sup mins ≡ supf1 px 1012 mins-is-spx : MinSUP.sup mins ≡ supf1 px
1024 mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl )) 1013 mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
1025 s<px : s o< px 1014 s<px : s o< px
1026 s<px = supf-inject0 supf1-mono ss<spx 1015 s<px = supf-inject0 supf1-mono ss<spx
1027 sf≤px : supf0 s o≤ px 1016 sf<px : supf0 s o< px
1028 sf≤px = subst (λ k → supf0 s o< k ) ? (ordtrans ? sfpx<x ) 1017 sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx
1029 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 1018 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
1030 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) 1019 csupf17 (init as refl ) = ZChain.csupf zc sf<px
1031 csupf17 (init as refl ) with osuc-≡< sf≤px 1020 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
1032 ... | case2 sf<px = ZChain.csupf zc sf<px 1021
1033 ... | case1 sf=px = ? 1022 ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px)
1023 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫
1024 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x)
1025 record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫ where
1026 z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
1027 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) (ChainP.fcy<sup is-sup fc)
1028 z11 : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1
1029 → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u )
1030 z11 {s} {z} lt fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x)))
1031 (ChainP.order is-sup lt0 (fcup fc s≤px )) where
1032 s<u : s o< u
1033 s<u = supf-inject0 supf1-mono lt
1034 s≤px : s o≤ px
1035 s≤px = ordtrans s<u (o<→≤ u≤x)
1036 lt0 : supf0 s o< supf0 u
1037 lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u≤x)) lt
1038 z12 : supf1 u ≡ u
1039 z12 = trans (sf1=sf0 (o<→≤ u≤x)) (ChainP.supu=u is-sup)
1040
1034 1041
1035 1042
1036 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where 1043 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
1037 field 1044 field
1038 tsup : MinSUP A (UnionCF A f mf ay supf0 z) 1045 tsup : MinSUP A (UnionCF A f mf ay supf0 z)