Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 901:6146d75131f5
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 09 Oct 2022 17:58:41 +0900 |
| parents | ac4daa43ef2a |
| children | 49594badc9b4 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 63 insertions(+), 244 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Oct 07 17:13:41 2022 +0900 +++ b/src/zorn.agda Sun Oct 09 17:58:41 2022 +0900 @@ -656,14 +656,6 @@ = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab - sb≤sx : supf b o≤ supf x - sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) - sb<sx : supf b o< supf x - sb<sx with osuc-≡< sb≤sx - ... | case2 lt = lt - ... | case1 sb=sx = ? where - -- b ≡ x - -- b o< px → a < * b → odef (UnionCF A f mf ay supf px) b m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) @@ -687,10 +679,6 @@ is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ ... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where - sb≤sx : supf b o≤ supf x - sb≤sx = ZChain.supf-mono zc (o<→≤ b<x ) - sb<sx : supf b o< supf x - sb<sx = ? m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b @@ -821,14 +809,6 @@ pchain : HOD pchain = UnionCF A f mf ay supf0 px - -- px o< supf0 px → UnionCF supf0 px ≡ UnionCF supf1 x - -- supf1 x ≡ supf0 px - -- px ≡ supf0 px → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x - -- supf1 x ≡ sup of ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) (= UnionCF supf1 x))) -- nsup ≥ supf0 px - -- supf0 px o< px → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x - -- nsup o≥ supf0 px → supf1 x ≡ nsup - -- nsup o< supf0 px → ? - supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b supf-mono = ZChain.supf-mono zc @@ -840,18 +820,12 @@ ... | case1 eq = case2 eq ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - zc4 : ZChain A f mf ay x --- supf px ≤ supf x - zc4 with trio< x (supf0 px) - ... | tri> ¬a ¬b c = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? - ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where - ... | tri≈ ¬a b ¬c = ? where - -- ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1 - -- ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where - - -- we are going to determine (supf x), which is not specified in previous zc - -- case1 : supf px ≡ px - -- supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and FClosure px - sfpx=px = ? + zc41 : supf0 px o≤ x → ZChain A f mf ay x + zc41 sfpx≤x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? + ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where + -- supf0 px is included by the chain + -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x + -- supf1 x ≡ sp1, which is not included now pchainpx : HOD pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z } ; odmax = & A ; <odmax = zc00 } where @@ -865,7 +839,7 @@ zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b zc02 {a} {b} ca fb = zc05 fb where zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px - zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) (sym sfpx=px) + zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) ? zc05 : {b : Ordinal } → FClosure A f px b → a <= b zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb )) ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) @@ -894,249 +868,94 @@ lt1 = subst₂ (λ j k → j < k ) *iso *iso lt ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp px f mf a b) - sup1 : MinSUP A pchainpx - sup1 = minsupP pchainpx zc01 ptotal + pcha : pchainpx ⊆' A + pcha (case1 lt) = proj1 lt + pcha (case2 fc) = A∋fc _ f mf fc - sp1 : Ordinal - sp1 = MinSUP.sup sup1 + sup1 : MinSUP A pchainpx + sup1 = minsupP pchainpx pcha ptotal + sp1 = MinSUP.sup sup1 supf1 : Ordinal → Ordinal supf1 z with trio< z px ... | tri< a ¬b ¬c = supf0 z - ... | tri≈ ¬a b ¬c = px --- supf px ≡ px - ... | tri> ¬a ¬b c = sp1 --- this may equal or larger then x, and sp1 ≡ supf x, is not included in UniofCF - - apx : odef A px - apx = subst (λ k → odef A k ) (sym sfpx=px) ( ZChain.asupf zc ) - - asupf1 : {z : Ordinal } → odef A (supf1 z ) - asupf1 {z} with trio< z px - ... | tri< a ¬b ¬c = ZChain.asupf zc - ... | tri≈ ¬a b ¬c = subst (λ k → odef A k ) (trans (cong supf0 b) (sym sfpx=px)) ( ZChain.asupf zc ) - ... | tri> ¬a ¬b c = MinSUP.asm sup1 + ... | tri≈ ¬a b ¬c = supf0 z + ... | tri> ¬a ¬b c = sp1 sf1=sf0 : {z : Ordinal } → z o≤ px → supf1 z ≡ supf0 z - sf1=sf0 {z} z<px with trio< z px + sf1=sf0 {z} z≤px with trio< z px ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = trans sfpx=px (cong supf0 (sym b)) - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z<px c ) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c ) - 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 (sf1=sf0 (o<→≤ (ordtrans≤-< z≤w a)))) refl ( supf-mono z≤w ) - ... | tri≈ ¬a refl ¬c with osuc-≡< z≤w - ... | case1 refl = o≤-refl0 zc17 where - zc17 : supf1 px ≡ px - zc17 with trio< px px - ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) - ... | case2 lt = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (o<→≤ lt))) (sym sfpx=px) ( supf-mono z≤w ) - supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px - ... | tri< a ¬b ¬c = zc19 where - zc21 : MinSUP A (UnionCF A f mf ay supf0 z) - zc21 = ZChain.minsup zc (o<→≤ a) - zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) - zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a) ux)) - zc19 : supf0 z o≤ sp1 - zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) - ... | tri≈ ¬a b ¬c = zc18 where - zc21 : MinSUP A (UnionCF A f mf ay supf0 z) - zc21 = ZChain.minsup zc (o≤-refl0 b) - zc20 : MinSUP.sup zc21 ≡ px - zc20 = begin - MinSUP.sup zc21 ≡⟨ sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) ⟩ - supf0 z ≡⟨ cong supf0 b ⟩ - supf0 px ≡⟨ sym sfpx=px ⟩ - px ∎ where open ≡-Reasoning - zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) - zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux)) - zc18 : px o≤ sp1 -- supf0 z ≡ px - zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) - ... | tri> ¬a ¬b c = o≤-refl - - supf-<1 : {z0 z1 : Ordinal} → supf1 z0 o< supf1 z1 → supf1 z0 << supf1 z1 - supf-<1 {z0} {z1} sz0<sz1 = zc21 where - z0<z1 : z0 o< z1 - z0<z1 = supf-inject0 supf-mono1 sz0<sz1 - zc26 : supf0 px <= sp1 - zc26 with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl )) - ... | case1 eq = case1 (trans (sym sfpx=px) eq ) - ... | case2 lt = case2 (subst (λ k → k << sp1 ) sfpx=px lt) - zc22 : ¬ px ≡ sp1 → supf0 px << sp1 - zc22 not with MinSUP.x<sup sup1 (case2 (init (subst (λ k → odef A k) (sym sfpx=px) (ZChain.asupf zc) ) refl )) - ... | case1 eq = ⊥-elim ( not eq ) -- px ≡ sp1 - ... | case2 lt = subst (λ k → k << sp1 ) sfpx=px lt - zc21 : supf1 z0 << supf1 z1 - zc21 with trio< z1 px - ... | tri< a ¬b ¬c = subst (λ k → k << supf0 z1) (sym (sf1=sf0 (o<→≤ (ordtrans z0<z1 a)))) - ( ZChain.supf-< zc (subst (λ k → k o< supf0 z1) (sf1=sf0 (o<→≤ (ordtrans z0<z1 a))) sz0<sz1 )) - ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j << k ) (sym (sf1=sf0 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 )))) (sym sfpx=px) - ( ZChain.supf-< zc (subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ (subst (λ k → z0 o< k) b z0<z1 ))) sfpx=px sz0<sz1 )) - ... | tri> ¬a ¬b px<z1 with trio< z0 px --- supf1 z1 ≡ sp1 - ... | tri< a ¬b ¬c = zc23 where - zc23 : supf0 z0 << sp1 - zc23 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ a) ) - ... | case1 eq = subst (λ k → k << sp1 ) (sym eq) (zc22 zc24) where - zc25 : px ≡ sp1 → supf0 z0 ≡ sp1 - zc25 px=sp1 = begin supf0 z0 ≡⟨ eq ⟩ - supf0 px ≡⟨ sym ( sfpx=px ) ⟩ - px ≡⟨ px=sp1 ⟩ - sp1 ∎ where open ≡-Reasoning - zc24 : ¬ px ≡ sp1 - zc24 eq1 = ⊥-elim (o<¬≡ (zc25 eq1) sz0<sz1 ) - ... | case2 lt with zc26 - ... | case1 eq = subst (λ k → supf0 z0 << k ) eq (ZChain.supf-< zc lt) - ... | case2 lt1 = ptrans (ZChain.supf-< zc lt) lt1 - ... | tri≈ ¬a b ¬c = subst (λ k → k << sp1 ) (sym sfpx=px) (zc22 zc23 ) where - zc23 : ¬ px ≡ sp1 - zc23 eq = ⊥-elim (o<¬≡ eq sz0<sz1 ) - ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl sz0<sz1 ) + sf1=sp1 : {z : Ordinal } → px o< z → supf1 z ≡ sp1 + sf1=sp1 {z} px<z with trio< z px + ... | tri< a ¬b ¬c = ⊥-elim ( o<> px<z a ) + ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) px<z ) + ... | tri> ¬a ¬b c = refl - 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 ) (sf1=sf0 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 (sf1=sf0 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 (fsuc _ fc) - zc21 (init asp refl ) with trio< u px | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 - ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where - zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → - FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where - zc19 : u o≤ px - zc19 = o<→≤ a - zc18 : s o≤ px - zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19 - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = case2 (init apx refl ) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? ⟫ ) - 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) ?) - record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans ((sf1=sf0 ?)) (ChainP.supu=u is-sup) } zc14 ⟫ where - zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 ?)) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ?) ss<spx) (fcup fc s≤px) ) where - s≤px : s o≤ px - s≤px = ? -- ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u≤x) - zc14 : FClosure A f (supf1 u) (supf0 u) - zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?) - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ?)) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 - ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where - zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) - zc18 : supf1 px ≡ px - zc18 = begin - supf1 px ≡⟨ sf1=sf0 o≤-refl ⟩ - supf0 px ≡⟨ cong supf0 (sym b) ⟩ - supf0 u ≡⟨ ChainP.supu=u is-sup ⟩ - u ≡⟨ b ⟩ - px ∎ where open ≡-Reasoning - 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)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) - ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where - zc19 : supf1 px ≡ supf0 u - zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) - s≤px : s o≤ px - s≤px = o<→≤ (supf-inject0 supf-mono1 ss<spx) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ? ⟫ ) - 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 ? - record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where - zc15 : supf1 px ≡ px - zc15 = trans (sf1=sf0 o≤-refl ) (sym sfpx=px) - zc14 : FClosure A f (supf1 px) px - zc14 = init (subst (λ k → odef A k) (sym zc15) asp) 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 ) - 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 supf-mono1 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) (sym sfpx=px)) ss<spx - -- (sf1=sf0 ?) (trans ? 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) + supf1-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b + supf1-mono {a} {b} a≤b with trio< b px + ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (o<→≤ (ordtrans≤-< a≤b a)))) refl ( supf-mono a≤b ) + ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (subst (λ k → a o≤ k) b a≤b))) refl ( supf-mono a≤b ) + supf1-mono {a} {b} a≤b | tri> ¬a ¬b c with trio< a px + ... | tri< a<px ¬b ¬c = zc19 where + zc21 : MinSUP A (UnionCF A f mf ay supf0 a) + zc21 = ZChain.minsup zc (o<→≤ a<px) + zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a<px) ux ) ) + zc19 : supf0 a o≤ sp1 + zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) + ... | tri≈ ¬a b ¬c = zc18 where + zc21 : MinSUP A (UnionCF A f mf ay supf0 a) + zc21 = ZChain.minsup zc (o≤-refl0 b) + zc20 : MinSUP.sup zc21 ≡ supf0 a + zc20 = sym (ZChain.supf-is-minsup zc (o≤-refl0 b)) + zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o≤-refl0 b) ux ) ) + zc18 : supf0 a o≤ sp1 + zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) + ... | tri> ¬a ¬b c = o≤-refl 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 : MinSUP A (UnionCF A f mf ay supf0 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 (sf1=sf0 (o<→≤ a)) (ZChain.supf-is-minsup zc (o<→≤ a)) } where + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (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 (sf1=sf0 (o≤-refl0 b)) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where + ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (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 = ? } + ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 + ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf1 {z1} sz1<x with trio< (supf0 z1) px - ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) (sym (sf1=sf0 z1≤px)) (case1 (ZChain.csupf zc a )) where + ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) ? (sym (sf1=sf0 (o<→≤ a) )) (case1 (ZChain.csupf zc a )) where z1≤px : z1 o≤ px - z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a )) - ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where - z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px - z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? )) - zc20 : supf0 px ≡ supf1 z1 - zc20 = begin - supf0 px ≡⟨ sym sfpx=px ⟩ - px ≡⟨ sym b ⟩ - supf0 z1 ≡⟨ sym (sf1=sf0 z1≤px) ⟩ - supf1 z1 ∎ where open ≡-Reasoning + z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) ? a )) + ... | tri≈ ¬a b ¬c = ? ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc21 , subst (λ k → z1 o< k ) (sym (Oprev.oprev=x op)) zc22 ⟫ ) where zc21 : px o< z1 - zc21 = ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c ) + zc21 = ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) ? c ) zc22 : z1 o< x -- c : px o< supf0 z1 - zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? ) + zc22 = ? -- supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? ) -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x - ... | tri< a ¬b ¬c = ? where + zc4 : ZChain A f mf ay x --- supf px ≤ supf x + zc4 with trio< x (supf0 px) + ... | tri> ¬a ¬b c = zc41 (o<→≤ c) + ... | tri≈ ¬a b ¬c = zc41 (o≤-refl0 (sym b)) + ... | tri< a ¬b ¬c = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? + ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where - -- case2 : px o< supf px - -- supf px is not MinSUP of previous chain , supf x ≡ supf px + -- supf0 px not is included by the chain + -- supf1 x ≡ supf0 px because of supfmax - -- record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono - -- ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where supf1 : Ordinal → Ordinal supf1 z with trio< z px ... | tri< a ¬b ¬c = supf0 z