Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 979:6229017a6176
chain is now u≤x again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 09 Nov 2022 05:00:56 +0900 |
| parents | 94357ced682d |
| children | 49cf50d451e1 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 76 insertions(+), 75 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Nov 09 03:14:40 2022 +0900 +++ b/src/zorn.agda Wed Nov 09 05:00:56 2022 +0900 @@ -273,15 +273,15 @@ data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z - ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : supf u o< supf x) ( is-sup : ChainP A f mf ay supf u ) + ch-is-sup : (u : Ordinal) {z : Ordinal } (u≤x : supf u o≤ supf x) ( is-sup : ChainP A f mf ay supf u ) ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z -- -- f (f ( ... (sup y))) f (f ( ... (sup z1))) -- / | / | -- / | / | --- sup y < sup z1 < sup z2 --- o< o< +-- sup y ≤ sup z1 ≤ sup z2 +-- o≤ o≤ -- data UChain is total chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) @@ -289,7 +289,7 @@ chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca + ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) with ChainP.fcy<sup supb fca ... | case1 eq with s≤fc (supf ub) f mf fcb ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * a ≡ * b @@ -297,14 +297,14 @@ ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where ct01 : * a < * b ct01 = subst (λ k → * k < * b ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where + ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u≤x supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where ct00 : * a < * (supf ub) ct00 = lt ct01 : * a < * b ct01 with s≤fc (supf ub) f mf fcb ... | case1 eq = subst (λ k → * a < k ) eq ct00 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt - ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb + ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb ... | case1 eq with s≤fc (supf ua) f mf fca ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * a ≡ * b @@ -312,7 +312,7 @@ ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where ct01 : * b < * a ct01 = subst (λ k → * k < * a ) (sym eq) lt - ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where + ct-ind xa xb {a} {b} (ch-is-sup ua u≤x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where ct00 : * b < * (supf ua) ct00 = lt ct01 : * b < * a @@ -402,7 +402,7 @@ chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = - ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (supf-mono a≤b ) ) is-sup fc ⟫ + ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x ? ) is-sup fc ⟫ record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where @@ -435,11 +435,11 @@ chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ - f-next {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x is-sup (fsuc _ fc ) ⟫ + f-next {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫ initial : {z : Ordinal } → odef chain z → * y ≤ * z initial {a} ⟪ aa , ua ⟫ with ua ... | ch-init fc = s≤fc y f mf fc - ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where + ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where zc7 : y <= supf u zc7 = ChainP.fcy<sup is-sup (init ay refl) f-total : IsTotalOrderSet chain @@ -490,35 +490,35 @@ → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x) → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ -UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫ where - u<x0 : u o< z - u<x0 = supf-inject0 supf-mono u<x - u<x1 : supf1 u o< supf1 z - u<x1 = subst (λ k → k o< supf1 z ) (eq<x u<x0) (ordtrans<-≤ u<x (lex o≤-refl ) ) +UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u≤x is-sup fc ⟫ = ⟪ az , ch-is-sup u ? cp1 fc1 ⟫ where + u≤x0 : u o< z + u≤x0 = supf-inject0 supf-mono ? + u≤x1 : supf1 u o< supf1 z + u≤x1 = subst (λ k → k o< supf1 z ) (eq<x u≤x0) (ordtrans<-≤ u≤x ? ) -- (lex o≤-refl ) ) fc1 : FClosure A f (supf1 u) x - fc1 = subst (λ k → FClosure A f k x ) (eq<x u<x0) fc + fc1 = subst (λ k → FClosure A f k x ) (eq<x u≤x0) fc uc01 : {s : Ordinal } → supf1 s o< supf1 u → s o< z uc01 {s} s<u with trio< s z ... | tri< a ¬b ¬c = a - ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02 s<u ) where -- (supf-mono (o<→≤ u<x0)) + ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02 s<u ) where -- (supf-mono (o<→≤ u≤x0)) uc02 : supf1 u o≤ supf1 s uc02 = begin - supf1 u <⟨ u<x1 ⟩ + supf1 u <⟨ u≤x1 ⟩ supf1 z ≡⟨ cong supf1 (sym b) ⟩ supf1 s ∎ where open o≤-Reasoning O ... | tri> ¬a ¬b c = ⊥-elim ( o≤> uc03 s<u ) where uc03 : supf1 u o≤ supf1 s uc03 = begin - supf1 u ≡⟨ sym (eq<x u<x0) ⟩ - supf u <⟨ u<x ⟩ + supf1 u ≡⟨ sym (eq<x u≤x0) ⟩ + supf u <⟨ ? ⟩ supf z ≤⟨ lex (o<→≤ c) ⟩ supf1 s ∎ where open o≤-Reasoning O cp1 : ChainP A f mf ay supf1 u - cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0) (ChainP.fcy<sup is-sup fc ) - ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x0) - (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u<x0)) s<u) + cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u≤x0) (ChainP.fcy<sup is-sup fc ) + ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u≤x0) + (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u≤x0)) s<u) (subst (λ k → FClosure A f k z ) (sym (eq<x (uc01 s<u) )) fc )) - ; supu=u = trans (sym (eq<x u<x0)) (ChainP.supu=u is-sup) } + ; supu=u = trans (sym (eq<x u≤x0)) (ChainP.supu=u is-sup) } 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 @@ -654,8 +654,8 @@ → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) - (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ + ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) + (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ supf = ZChain.supf zc @@ -670,7 +670,7 @@ zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where + ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s zc07 = fc zc06 : supf u ≡ u @@ -681,7 +681,7 @@ zc04 : odef (UnionCF A f mf ay supf b) (f x) zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ - ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫ + ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) order {b} {s} {z1} b<z ss<sb fc = zc04 where zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) @@ -705,7 +705,7 @@ is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup - = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where b<A : b o< & A b<A = z09 ab b<x : b o< x @@ -731,7 +731,7 @@ is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b is-max {a} {b} ua sb<sx 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 sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + ... | case2 y<b = ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) b<x : b o< x @@ -968,17 +968,17 @@ 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 su<sx is-sup fc ⟫ = zc21 fc where - u<x : u o< x - u<x = supf-inject0 supf1-mono su<sx + u≤x : u o< x + u≤x = supf-inject0 supf1-mono ? -- su<sx u≤px : u o≤ px - u≤px = zc-b<x _ u<x + u≤px = zc-b<x _ u≤x 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₁) ⟫ + ... | 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< (supf0 u) (supf0 px) | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17 + ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where u<px : u o< px u<px = ZChain.supf-inject zc a @@ -993,41 +993,41 @@ 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<→≤ u<px)) ( ChainP.fcy<sup is-sup fc ) ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b ))) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x ⟫ ) zc35 : {z : Ordinal} → ¬ (supf0 px ≡ px) → odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z zc35 {z} ne ⟪ ua1 , ch-init fc ⟫ = ⟪ ua1 , ch-init fc ⟫ - zc35 {z} ne ⟪ ua1 , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono u<x)) ) + zc35 {z} ne ⟪ ua1 , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (supf-inject0 supf1-mono ?)) ) ... | case1 eq = zc34 where - u<x0 : u o≤ px - u<x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono u<x ) + u≤x0 : u o≤ px + u≤x0 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) (supf-inject0 supf1-mono ? ) zc34 : odef (UnionCF A f mf ay supf0 x) z zc34 with trio< (supf0 px) px ... | tri< sf0px<px ¬b ¬c = cp3 ( subst ( λ k → FClosure A f k z) - (trans (trans (sf1=sf0 u<x0) eq) (ZChain.supfmax zc px<x) ) fc) where + (trans (trans (sf1=sf0 u≤x0) eq) (ZChain.supfmax zc px<x) ) fc) where cp3 : {z : Ordinal } → FClosure A f (supf0 px) z → odef (UnionCF A f mf ay supf0 x) z cp3 (init uz refl) = chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc sf0px<px) cp3 (fsuc uz fc) = ZChain.f-next zc (cp3 fc) ... | tri≈ ¬a b ¬c = ⊥-elim (ne b) ... | tri> ¬a ¬b px<sf0px = ⊥-elim (¬p<x<op ⟪ cp5 , cp4 ⟫ ) where cp4 : u o< osuc px - cp4 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ( supf-inject0 supf1-mono u<x ) + cp4 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ( supf-inject0 supf1-mono ? ) cp5 : px o< u cp5 = subst (λ k → px o< k ) ( begin supf0 px ≡⟨ sym (ZChain.supfmax zc px<x) ⟩ supf0 x ≡⟨ sym eq ⟩ - supf0 u ≡⟨ sym (sf1=sf0 u<x0) ⟩ + supf0 u ≡⟨ sym (sf1=sf0 u≤x0) ⟩ supf1 u ≡⟨ ChainP.supu=u is-sup ⟩ u ∎ ) px<sf0px where open ≡-Reasoning - ... | case2 u<x1 = ⟪ ua1 , ch-is-sup u u<x1 cp1 fc1 ⟫ where - u<x0 : u o< x - u<x0 = supf-inject0 supf1-mono u<x -- supf0 u o≤ px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px + ... | case2 u≤x1 = ⟪ ua1 , ch-is-sup u ? cp1 fc1 ⟫ where + u≤x0 : u o< x + u≤x0 = supf-inject0 supf1-mono ? -- supf0 u o≤ px ≡ supf0 px → supf0 u ≡ supf0 px ∨ u o< px sf0u=sf1u : supf0 u ≡ supf1 u - sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 )) + sf0u=sf1u = sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 )) cp2 : {s : Ordinal } → supf0 s o< supf0 u → supf0 s ≡ supf1 s cp2 {s} ss<su = sym ( sf1=sf0 ( begin s <⟨ ZChain.supf-inject zc ss<su ⟩ - u ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ⟩ + u ≤⟨ subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 ⟩ px ∎ )) where open o≤-Reasoning O fc1 : FClosure A f (supf0 u) z fc1 = subst (λ k → FClosure A f k z ) (sym sf0u=sf1u) fc @@ -1036,7 +1036,7 @@ ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym sf0u=sf1u) (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (cp2 s<u) sf0u=sf1u s<u) (subst (λ k → FClosure A f k z ) (cp2 s<u) fc )) - ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x0 ))) (ChainP.supu=u is-sup) } + ; supu=u = trans (sym (sf1=sf0 (subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u≤x0 ))) (ChainP.supu=u is-sup) } zc33 : {z : Ordinal} → ¬ (supf0 px o< sp1) → odef (UnionCF A f mf ay supf1 x) z → odef (UnionCF A f mf ay supf0 x) z zc33 {z} lt = UChain⊆ A f mf ay supf1-mono (λ lt → sym (sf=eq lt)) sf≤0 where @@ -1063,20 +1063,20 @@ zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where u<px : u o< px - u<px = ZChain.supf-inject zc su<sx - u<x : u o< x - u<x = ordtrans u<px px<x + u<px = ZChain.supf-inject zc ? -- su<sx + u≤x : u o< x + u≤x = ordtrans u<px px<x u≤px : u o≤ px u≤px = o<→≤ u<px s1u<s1x : supf1 u o< supf1 x - s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) su<sx) (supf1-mono (o<→≤ px<x) ) + s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) ?) (supf1-mono (o<→≤ px<x) ) 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₁) ⟫ + ... | ⟪ 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 - s1u<s1x + ? -- s1u<s1x record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 u≤px ) (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) @@ -1088,7 +1088,7 @@ zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 u≤px)) asp) (sf1=sf0 u≤px) 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 u≤px )) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (subst (λ k → supf1 k o< supf1 x) b s1u<s1x) record { fcy<sup = zc13 + ... | 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 ) @@ -1113,8 +1113,8 @@ zc21 : {z1 : Ordinal } → FClosure A f (supf0 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 zc18 + ... | ⟪ 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 ) (sfpx=px) @@ -1179,6 +1179,7 @@ (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px)))) -- px o< z1 , px o≤ supf1 z1 --> px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1 + -- supf1 px ≡ sp1 o< supf1 x csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf1 {z1} sz1<x = csupf2 where @@ -1320,7 +1321,7 @@ zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) x≤sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) x≤sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? - x≤sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? )) + x≤sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u≤x) ? )) ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where zc14 : u ≡ osuc px zc14 = begin @@ -1444,9 +1445,9 @@ * a < * b → odef (UnionCF A f mf ay supf x) b is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ? -- ⟪ ab , + ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ? -- ⟪ ab , -- subst (λ k → UChain A f mf ay supf x k ) - -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ + -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ zc70 : HasPrev A pchain f x → ¬ xSUP pchain f x zc70 pr xsup = ? @@ -1460,23 +1461,23 @@ pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where + zc10 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc12 fc where zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z zc12 (fsuc x fc) with zc12 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫ zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where + zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z zc13 (fsuc x fc) with zc13 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ - ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ zc13 (init asu su=z ) with trio< u x ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫ ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c ) + ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u≤x c ) sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) sup {z} z≤x with trio< z x ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} ) @@ -1674,7 +1675,7 @@ z31 : ( * (cf nmx mc) ≡ * mc ) ∨ ( * (cf nmx mc) < * mc ) z31 = <=to≤ ( MinSUP.x≤sup msp1 (subst (λ k → odef (ZChain.chain zc) (cf nmx k)) (sym x=fy) ⟪ proj2 (cf-is-≤-monotonic nmx _ (proj2 (cf-is-≤-monotonic nmx _ ua1 ) )) , ch-init (fsuc _ (fsuc _ fc)) ⟫ )) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where + not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u≤x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where z30 : * mc < * (cf nmx mc) z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) z31 : ( supf mc ≡ mc ) ∨ ( * (supf mc) < * mc ) @@ -1682,7 +1683,7 @@ z32 : * (supf mc) < * (cf nmx (cf nmx y)) z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 ) z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) - z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc _ fc ))) + z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A ? (fsuc _ ( fsuc _ fc ))) is-sup : IsSUP A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) } @@ -1695,16 +1696,16 @@ z32 = ZChain.fcy<sup zc (o<→≤ mc<A) (fsuc _ (fsuc _ fc)) z31 : ( * (cf nmx d) ≡ * d ) ∨ ( * (cf nmx d) < * d ) z31 = case2 ( subst (λ k → * (cf nmx k) < * d ) (sym x=fy) ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) - not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where + not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u≤x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d) z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p z48 : supf mc << d z48 = sc<<d {mc} asc spd z53 : supf u o< supf (& A) - z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) ) + z53 = ordtrans<-≤ u≤x ? z52 : ( u ≡ mc ) ∨ ( u << mc ) z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) - , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ + , ch-is-sup u ? is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ z51 : supf u o≤ supf mc z51 = or z52 (λ le → o≤-refl0 (z56 le) ) z57 where z56 : u ≡ mc → supf u ≡ supf mc @@ -1716,7 +1717,7 @@ z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc _ fc )) z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) ) - z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc _ fc )) + z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A ? (fsuc _ ( fsuc _ fc )) z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1 → * (cf nmx (cf nmx y)) < * d1 @@ -1743,13 +1744,13 @@ z22 {a} ⟪ aa , ch-init fc ⟫ = case2 ( ( ftrans<=-< z32 ( sc<<d {mc} asc spd ) )) where z32 : ( a ≡ supf mc ) ∨ ( * a < * (supf mc) ) z32 = ZChain.fcy<sup zc (o<→≤ mc<A) fc - z22 {a} ⟪ aa , ch-is-sup u u<x is-sup1 fc ⟫ = tri u (supf mc) + z22 {a} ⟪ aa , ch-is-sup u u≤x is-sup1 fc ⟫ = tri u (supf mc) z60 z61 ( λ sc<u → ⊥-elim ( o≤> ( subst (λ k → k o≤ supf mc) (ChainP.supu=u is-sup1) z51) sc<u )) where z53 : supf u o< supf (& A) - z53 = ordtrans<-≤ u<x (ZChain.supf-mono zc (o<→≤ d<A) ) + z53 = ordtrans<-≤ u≤x ? z52 : ( u ≡ mc ) ∨ ( u << mc ) z52 = MinSUP.x≤sup msp1 ⟪ subst (λ k → odef A k ) (ChainP.supu=u is-sup1) (A∋fcs _ _ (cf-is-≤-monotonic nmx) fc) - , ch-is-sup u z53 is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ + , ch-is-sup u ? is-sup1 (init (ZChain.asupf zc) (ChainP.supu=u is-sup1)) ⟫ z56 : u ≡ mc → supf u ≡ supf mc z56 eq = cong supf eq z57 : u << mc → supf u o≤ supf mc @@ -1763,7 +1764,7 @@ (subst (λ k → k o< supf mc) (sym (ChainP.supu=u is-sup1)) u<smc) fc ) smc<<d ) z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d ) z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) ) - -- u<x : ZChain.supf zc u o< ZChain.supf zc d + -- u≤x : ZChain.supf zc u o< ZChain.supf zc d -- supf u o< supf c → order sd=d : supf d ≡ d