Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1042:912ca4abe806
pxhainx conditon is requied?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Dec 2022 09:15:12 +0900 |
| parents | f12a9b4066a0 |
| children | fd26e0c4e648 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 127 insertions(+), 119 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Dec 03 16:57:15 2022 +0900 +++ b/src/zorn.agda Sun Dec 04 09:15:12 2022 +0900 @@ -23,7 +23,7 @@ import BAlgbra open import Data.Nat hiding ( _<_ ; _≤_ ) -open import Data.Nat.Properties +open import Data.Nat.Properties open import nat @@ -76,7 +76,7 @@ ftrans<-≤ : {x y z : Ordinal } → x << y → y ≤ z → x << z ftrans<-≤ {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y -ftrans<-≤ {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt +ftrans<-≤ {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO (sym a=b) b<a @@ -168,7 +168,7 @@ fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) → suc j ≡ fcn s mf cy1 → * (f x) ≡ * y1 fc03 y1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x) fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) ) - ... | case1 eq = trans ( fc03 y1 cy1 j=y1 ) (cong (*) eq) + ... | case1 eq = trans ( fc03 y1 cy1 j=y1 ) (cong (*) eq) ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where fc05 : * x ≡ * y1 fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1) @@ -258,7 +258,7 @@ -- this means sup z1 is the Maximal, so f is <-monotonic if we have no Maximal. -- -fc-stop : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal } +fc-stop : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal } → (aa : odef A a ) →( {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a fc-stop A f mf {a} {b} aa x≤sup a=b with x≤sup (fsuc a (init aa refl )) ... | case1 eq = trans eq (sym a=b) @@ -269,16 +269,16 @@ ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) --- Union of supf z and FClosure A f y +-- Union of supf z and FClosure A f y -data UChain { A : HOD } { f : Ordinal → Ordinal } {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y ) +data UChain { A : HOD } { f : Ordinal → Ordinal } {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y ) (x : Ordinal) : (z : Ordinal) → Set n where ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD UnionCF A f ay supf x - = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ; + = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } @@ -324,8 +324,8 @@ chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b → odef (UnionCF A f ay supf a) c → odef (UnionCF A f ay supf b) c -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 ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ +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 ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u 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 @@ -340,7 +340,7 @@ supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z - is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) + is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z → IsSUP A (UnionCF A f ay supf b) b ∧ (¬ HasPrev A (UnionCF A f ay supf b) f b ) → supf b ≡ b @@ -352,14 +352,14 @@ chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl) ⟫ - mf : ≤-monotonic-f A f + mf : ≤-monotonic-f A f mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where mf00 : * x < * (f x) mf00 = proj1 ( mf< x ax ) f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a) - f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua) , ch-init (fsuc _ fc) ⟫ - f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua) , ch-is-sup u su<x su=u (fsuc _ fc) ⟫ + f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua) , ch-init (fsuc _ fc) ⟫ + f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua) , ch-is-sup u su<x su=u (fsuc _ fc) ⟫ supf-inject : {x y : Ordinal } → supf x o< supf y → x o< y supf-inject {x} {y} sx<sy with trio< x y @@ -382,7 +382,7 @@ supf-is-minsup _ = refl -- different from order because y o< supf - fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) + fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) fcy<sup {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) @@ -390,7 +390,7 @@ initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x → y ≤ x initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc - initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc) + initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc) f-total : IsTotalOrderSet chain f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = @@ -400,35 +400,35 @@ ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) a₁ fca ) (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) - ct00 = cong (*) eq1 - ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) - fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb + ct00 = cong (*) eq1 + ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) + fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb fc-total | tri> ¬a ¬b c with ≤-ftrans (order (o<→≤ sua<x) c fcb ) (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) - ct00 = cong (*) (sym eq1) + ct00 = cong (*) (sym eq1) ... | case2 b<a = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where ft01 : (& a) ≤ (& b) → Tri ( a < b) ( a ≡ b) ( b < a ) ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where - a=b : a ≡ b + a=b : a ≡ b a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq) ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) where - a<b : a < b + a<b : a < b a<b = subst₂ (λ j k → j < k ) *iso *iso lt ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb)) f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where ft01 : (& b) ≤ (& a) → Tri ( a < b) ( a ≡ b) ( b < a ) ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where - a=b : a ≡ b + a=b : a ≡ b a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym eq)) ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where - b<a : b < a + b<a : b < a b<a = subst₂ (λ j k → j < k ) *iso *iso lt ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca)) - f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = + f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp y f mf fca fcb ) IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp @@ -444,10 +444,10 @@ fsp≤sp : f sp ≤ sp fsp≤sp = subst (λ k → f k ≤ sp ) (sym (HasPrev.x=fy hp)) im00 - supf-¬hp : {x : Ordinal } → x o≤ z + supf-¬hp : {x : Ordinal } → x o≤ z → ( {a : Ordinal } → odef A a → a << f a ) → ¬ ( HasPrev A (UnionCF A f ay supf x) f (supf x) ) - supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → + supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → (subst (λ k → w ≤ k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b @@ -458,7 +458,7 @@ su<b : u o< b su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) z52 : supf (supf b) ≡ supf b - z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ + z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b) -- the condition of cfcs is satisfied, this is obvious @@ -479,27 +479,27 @@ record IChain (A : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where field - i : Ordinal + i : Ordinal i<x : i o< x - fc : FClosure A f (supfz i<x) z + fc : FClosure A f (supfz i<x) z -- -- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup -- supf-unique : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) - {y xa xb : Ordinal} → (ay : odef A y) → (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb ) + {y xa xb : Ordinal} → (ay : odef A y) → (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb ) → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa where supfa = ZChain.supf za supfb = ZChain.supf zb ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x ind x prev x≤xa = sxa=sxb where - ma = ZChain.minsup za x≤xa + ma = ZChain.minsup za x≤xa mb = ZChain.minsup zb (OrdTrans x≤xa xa≤xb ) spa = MinSUP.sup ma spb = MinSUP.sup mb sax=spa : supfa x ≡ spa - sax=spa = ZChain.supf-is-minsup za x≤xa + sax=spa = ZChain.supf-is-minsup za x≤xa sbx=spb : supfb x ≡ spb sbx=spb = ZChain.supf-is-minsup zb (OrdTrans x≤xa xa≤xb ) sxa=sxb : supfa x ≡ supfb x @@ -509,11 +509,11 @@ begin supfb x ≡⟨ sbx=spb ⟩ spb ≤⟨ MinSUP.minsup mb (MinSUP.as ma) (λ {z} uzb → MinSUP.x≤sup ma (z53 uzb)) ⟩ - spa ≡⟨ sym sax=spa ⟩ - supfa x ∎ ) a ) where + spa ≡⟨ sym sax=spa ⟩ + supfa x ∎ ) a ) where open o≤-Reasoning O z53 : {z : Ordinal } → odef (UnionCF A f ay (ZChain.supf zb) x) z → odef (UnionCF A f ay (ZChain.supf za) x) z - z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ + z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ⟪ as , ch-is-sup u u<x (trans ua=ub su=u) z55 ⟫ where ua=ub : supfa u ≡ supfb u ua=ub = prev u u<x (ordtrans u<x x≤xa ) @@ -524,10 +524,10 @@ supfa x ≡⟨ sax=spa ⟩ spa ≤⟨ MinSUP.minsup ma (MinSUP.as mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩ spb ≡⟨ sym sbx=spb ⟩ - supfb x ∎ ) c ) where + supfb x ∎ ) c ) where open o≤-Reasoning O z53 : {z : Ordinal } → odef (UnionCF A f ay (ZChain.supf za) x) z → odef (UnionCF A f ay (ZChain.supf zb) x) z - z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ + z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ⟪ as , ch-is-sup u u<x (trans ub=ua su=u) z55 ⟫ where ub=ua : supfb u ≡ supfa u ub=ua = sym ( prev u u<x (ordtrans u<x x≤xa )) @@ -606,9 +606,9 @@ S = supP B B⊆A total s1 = & (SUP.sup S) m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 ) - m05 {w} bw with SUP.x≤sup S bw - ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (trans &iso eq)) - ... | case2 lt = case2 lt + m05 {w} bw with SUP.x≤sup S bw + ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (trans &iso eq)) + ... | case2 lt = case2 lt m02 : MinSUP A B m02 = dont-or (m00 (& A)) m03 @@ -659,7 +659,7 @@ supf = ZChain.supf zc zc1 : (x : Ordinal ) → x o≤ & A → ZChain1 A f mf< ay zc x - zc1 x x≤A with Oprev-p x + zc1 x x≤A with Oprev-p x ... | yes op = record { is-max = is-max } where px = Oprev.oprev op is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a → @@ -682,7 +682,7 @@ ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x ) m17 = ZChain.minsup zc x≤A - m18 : supf x ≡ MinSUP.sup m17 + m18 : supf x ≡ MinSUP.sup m17 m18 = ZChain.supf-is-minsup zc x≤A m10 : f (supf b) ≡ supf b m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where @@ -722,7 +722,7 @@ ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x ) m17 = ZChain.minsup zc x≤A - m18 : supf x ≡ MinSUP.sup m17 + m18 : supf x ≡ MinSUP.sup m17 m18 = ZChain.supf-is-minsup zc x≤A m10 : f (supf b) ≡ supf b m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where @@ -799,7 +799,7 @@ ... | 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 ⟫ ) - mf : ≤-monotonic-f A f + mf : ≤-monotonic-f A f mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where mf00 : * x < * (f x) mf00 = proj1 ( mf< x ax ) @@ -920,7 +920,7 @@ sf≤ {z} x≤z with trio< z px ... | tri< a ¬b ¬c = ⊥-elim ( o<> (osucc a) (subst (λ k → k o≤ z) (sym (Oprev.oprev=x op)) x≤z ) ) ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x )) - ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c) + ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c) (supf1-mono (o<→≤ c )) -- px o<z → supf x ≡ supf0 px ≡ supf1 px o≤ supf1 z @@ -931,22 +931,22 @@ sfpx<x : sp1 o≤ x → supf0 px o< x sfpx<x sp1≤x with trio< (supf0 px) x - ... | tri< a ¬b ¬c = a - ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where + ... | tri< a ¬b ¬c = a + ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case m12 : supf0 px ≡ sp1 m12 with osuc-≡< m13 ... | case1 eq = eq - ... | case2 lt = ⊥-elim ( o≤> sp1≤x (subst (λ k → k o< sp1) spx=x lt )) + ... | case2 lt = ⊥-elim ( o≤> sp1≤x (subst (λ k → k o< sp1) spx=x lt )) m10 : f (supf0 px) ≡ supf0 px m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1) - m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc) + m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc) ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp1≤x ))) -- x o< supf0 px o≤ sp1 ≤ x -- this is a kind of maximality, so we cannot prove this without <-monotonicity -- - cfcs : {a b w : Ordinal } + cfcs : {a b w : Ordinal } → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w cfcs {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px ... | case2 px≤sa = z50 where @@ -963,27 +963,27 @@ sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x spx=sa : supf0 px ≡ supf0 a spx=sa = begin - supf0 px ≡⟨ cong supf0 px=sa ⟩ + supf0 px ≡⟨ cong supf0 px=sa ⟩ supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc a≤px sa≤px ⟩ supf0 a ∎ where open ≡-Reasoning z51 : supf0 px o< b - z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩ - supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ + z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩ + supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ supf1 a ∎ )) sa<b where open ≡-Reasoning z52 : supf1 a ≡ supf1 (supf0 px) - z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ - supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px sa≤px ) ⟩ - supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ - supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ + z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ + supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px sa≤px ) ⟩ + supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ + supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ supf1 (supf0 px) ∎ where open ≡-Reasoning z53 : supf1 (supf0 px) ≡ supf0 px z53 = begin - supf1 (supf0 px) ≡⟨ cong supf1 spx=sa ⟩ - supf1 (supf0 a) ≡⟨ sf1=sf0 sa≤px ⟩ - supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩ - supf0 px ∎ where open ≡-Reasoning + supf1 (supf0 px) ≡⟨ cong supf1 spx=sa ⟩ + supf1 (supf0 a) ≡⟨ sf1=sf0 sa≤px ⟩ + supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩ + supf0 px ∎ where open ≡-Reasoning cp : UChain ay b w - cp = ch-is-sup (supf0 px) z51 z53 (subst (λ k → FClosure A f k w) z52 fc) + cp = ch-is-sup (supf0 px) z51 z53 (subst (λ k → FClosure A f k w) z52 fc) ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫ ) where z53 : supf1 a o< x z53 = ordtrans<-≤ sa<b b≤x @@ -991,22 +991,22 @@ ... | tri< a<px ¬b ¬c = z50 where z50 : odef (UnionCF A f ay supf1 b) w z50 with osuc-≡< b≤x - ... | case2 lt with ZChain.cfcs zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + ... | case2 lt with ZChain.cfcs zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc + ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ ... | ⟪ az , ch-is-sup u u<b su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc u≤px ) ⟫ where u≤px : u o≤ px u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ u<b b≤x ) u<x : u o< x - u<x = ordtrans<-≤ u<b b≤x - z50 | case1 eq with ZChain.cfcs zc a<px o≤-refl sa<px fc - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + u<x = ordtrans<-≤ u<b b≤x + z50 | case1 eq with ZChain.cfcs zc a<px o≤-refl sa<px fc + ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ ... | ⟪ az , ch-is-sup u u<px su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc (o<→≤ u<px)) ⟫ where -- u o< px → u o< b ? u<b : u o< b u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc ) u<x : u o< x u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc ) ... | tri≈ ¬a a=px ¬c = csupf1 where - -- a ≡ px , b ≡ x, sp o≤ x + -- a ≡ px , b ≡ x, sp o≤ x px<b : px o< b px<b = subst₂ (λ j k → j o< k) a=px refl a<b b=x : b ≡ x @@ -1019,14 +1019,18 @@ z53 : odef A w z53 = A∋fc {A} _ f mf fc csupf1 : odef (UnionCF A f ay supf1 b) w - csupf1 = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) (sfpx<x ?)) z52 fc1 ⟫ where - spx = supf0 px - spx≤px : supf0 px o≤ px - spx≤px = zc-b<x _ (sfpx<x ?) + csupf1 with zc43 px (supf0 px) + ... | case2 spx≤px = ⟪ z53 , ch-is-sup (supf0 px) z54 z52 fc1 ⟫ where + z54 : supf0 px o< b + z54 = subst (λ k → supf0 px o< k ) (trans (Oprev.oprev=x op) (sym b=x) ) spx≤px z52 : supf1 (supf0 px) ≡ supf0 px - z52 = trans (sf1=sf0 (zc-b<x _ (sfpx<x ?))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (sfpx<x ?) ) ) - fc1 : FClosure A f (supf1 spx) w + z52 = trans (sf1=sf0 spx≤px ) ( ZChain.supf-idem zc o≤-refl spx≤px ) + fc1 : FClosure A f (supf1 (supf0 px)) w fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc + ... | case1 px<spx = ⊥-elim (¬p<x<op ⟪ px<spx , z54 ⟫ ) where -- supf1 px o≤ spuf1 x → supf1 px ≡ x o< x + z54 : supf0 px o≤ px + z54 = subst₂ (λ j k → supf0 j o< k ) a=px (trans b=x (sym (Oprev.oprev=x op))) sa<b + ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x zc11 : {z : Ordinal} → odef (UnionCF A f ay supf1 x) z → odef pchainpx z @@ -1037,13 +1041,13 @@ ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | case1 ⟪ ua1 , ch-is-sup u u<x su=u fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫ ... | case2 fc = case2 (fsuc _ fc) - zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) + zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) ... | tri< a ¬b ¬c = case1 ⟪ asp , ch-is-sup u u<px (trans (sym (sf1=sf0 (o<→≤ u<px))) su=u )(init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where u<px : u o< px u<px = ZChain.supf-inject zc a asp0 : odef A (supf0 u) asp0 = ZChain.asupf zc - ... | tri≈ ¬a b ¬c = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) + ... | tri≈ ¬a b ¬c = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 (zc-b<x _ u<x)) 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 ⟫ ) @@ -1051,7 +1055,7 @@ is-minsup {z} z≤x with osuc-≡< z≤x ... | case1 z=x = record { as = zc22 ; x≤sup = z23 ; minsup = z24 } where px<z : px o< z - px<z = subst (λ k → px o< k) (sym z=x) px<x + px<z = subst (λ k → px o< k) (sym z=x) px<x zc22 : odef A (supf1 z) zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z )) ( MinSUP.as sup1 ) z26 : supf1 px ≤ supf1 x @@ -1059,29 +1063,33 @@ z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z z23 {w} uz with zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz ) ... | case1 uz = ≤-ftrans z25 (subst₂ (λ j k → j ≤ supf1 k) (sf1=sf0 o≤-refl) (sym z=x) z26 ) where - z25 : w ≤ supf0 px - z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz + z25 : w ≤ supf0 px + z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz ... | case2 fc = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (case2 fc) ) - z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s ) + z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s ) → supf1 z o≤ s z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where - z25 : {w : Ordinal } → odef pchainpx w → w ≤ s + z25 : {w : Ordinal } → odef pchainpx w → w ≤ s z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where - z28 : supf0 px o< z -- supf0 px ≡ supf1 px o≤ supf1 x o≤ + -- z=x , supf0 px o< x + z28 : supf0 px o< z -- supf0 px ≡ supf1 px o≤ supf1 x ≡ sp1 o≤ x ≡ z z28 = subst (λ k → supf0 px o< k) (sym z=x) (sfpx<x ?) - z29 : supf0 px o≤ px + z29 : supf0 px o≤ px z29 = zc-b<x _ (sfpx<x ?) z27 : supf1 (supf0 px) ≡ supf0 px z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 ) fc1 : FClosure A f (supf1 (supf0 px)) w fc1 = subst (λ k → FClosure A f k w) (sym z27) fc + -- x o≤ supf0 px o≤ supf0 z ≡ supf0 x ≡ sp1 + -- x o≤ supf0 px o≤ supf0 x ≡ sp1 + -- fc : FClosure A f (supf0 px) w -- ¬ ( supf0 px o< x ) → ¬ odef ( UnionCF A f ay supf1 z ) w z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫ z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫) = sup ⟪ ua , ch-is-sup u u<z (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where - u≤px : u o< osuc px - u≤px = ordtrans u<x <-osuc - u<z : u o< z - u<z = ordtrans u<x (subst (λ k → px o< k ) (sym z=x) px<x ) + u≤px : u o< osuc px + u≤px = ordtrans u<x <-osuc + u<z : u o< z + u<z = ordtrans u<x (subst (λ k → px o< k ) (sym z=x) px<x ) ... | case2 z<x = record { as = zc22 ; x≤sup = z23 ; minsup = z24 } where z≤px = zc-b<x _ z<x m = ZChain.is-minsup zc z≤px @@ -1089,16 +1097,16 @@ zc22 = subst (λ k → odef A k ) (sym (sf1=sf0 z≤px)) ( IsMinSUP.as m ) z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z z23 {w} ⟪ ua , ch-init fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px)) ( ZChain.fcy<sup zc z≤px fc ) - z23 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px)) + z23 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = subst (λ k → w ≤ k ) (sym (sf1=sf0 z≤px)) (IsMinSUP.x≤sup m ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px )) su=u) (fcup fc u≤px ) ⟫ ) where u≤px : u o≤ px u≤px = ordtrans u<x z≤px z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s ) → supf1 z o≤ s z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sf0 z≤px)) ( IsMinSUP.minsup m as z25 ) where - z25 : {w : Ordinal } → odef ( UnionCF A f ay supf0 z ) w → w ≤ s + z25 : {w : Ordinal } → odef ( UnionCF A f ay supf0 z ) w → w ≤ s z25 {w} ⟪ ua , ch-init fc ⟫ = sup ⟪ ua , ch-init fc ⟫ - z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = sup ⟪ ua , ch-is-sup u u<x + z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = sup ⟪ ua , ch-is-sup u u<x (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where u≤px : u o≤ px u≤px = ordtrans u<x z≤px @@ -1106,11 +1114,11 @@ order : {a b : Ordinal} {w : Ordinal} → b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b order {a} {b} {w} b≤x a<b fc with trio< b px - ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) )) + ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) )) ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b ))) ... | tri> ¬a ¬b px<b with trio< a px ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) sfpx≤sp1 -- supf1 a ≡ supf0 a - ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc )) + ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc )) ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where -- supf1 a ≡ sp1 zc22 : a o< osuc px zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x) @@ -1126,21 +1134,21 @@ ... | case1 eq = sym (eq) ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) zc31 : sp1 o≤ b - zc31 = MinSUP.minsup sup1 ab zc32 where - zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) + zc31 = MinSUP.minsup sup1 ab zc32 where + zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) zc32 = ? - + ... | no lim with trio< x o∅ - ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) + ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ? - ; supfmax = ? ; is-minsup = ? ; cfcs = ? } + ; supfmax = ? ; is-minsup = ? ; cfcs = ? } ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where - -- mf : ≤-monotonic-f A f + -- mf : ≤-monotonic-f A f -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust - mf : ≤-monotonic-f A f + mf : ≤-monotonic-f A f mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where mf00 : * x < * (f x) mf00 = proj1 ( mf< x ax ) @@ -1161,14 +1169,14 @@ aic : {z : Ordinal } → IChain A f supfz z → odef A z aic {z} ic = A∋fc _ f mf (IChain.fc ic ) - zeq : {xa xb z : Ordinal } - → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa - → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z - zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = supf-unique A f mf< ay xa≤xb + zeq : {xa xb z : Ordinal } + → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa + → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z + zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = supf-unique A f mf< ay xa≤xb (pzc xa<x) (pzc xb<x) z≤xa - iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y - iceq refl = cong supfz o<-irr + iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y + iceq refl = cong supfz o<-irr ifc≤ : {za zb : Ordinal } ( ia : IChain A f supfz za ) ( ib : IChain A f supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib ) → FClosure A f (ZChain.supf (pzc (ob<x lim (IChain.i<x ib))) (IChain.i ia)) za @@ -1178,13 +1186,13 @@ ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 with trio< (IChain.i ia) (IChain.i ib) - ... | tri< ia<ib ¬b ¬c with + ... | tri< ia<ib ¬b ¬c with ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib)) ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * (& a) ≡ * (& b) ct00 = cong (*) eq1 - ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1) - uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) + ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1) + uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) uz01 | tri> ¬a ¬b ib<ia with ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia)) ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where @@ -1198,7 +1206,7 @@ supf1 : Ordinal → Ordinal supf1 z with trio< z x - ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z + ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z ... | tri≈ ¬a b ¬c = spu ... | tri> ¬a ¬b c = spu @@ -1212,7 +1220,7 @@ uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = ? -- chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) - sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc (ob<x lim a)) z + sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc (ob<x lim a)) z sf1=sf {z} z<x with trio< z x ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x) @@ -1244,7 +1252,7 @@ cfcs : {a b w : Ordinal } → a o< b → b o≤ x → supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w cfcs {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x - ... | case1 b=x with trio< a x + ... | case1 b=x with trio< a x ... | tri< a<x ¬b ¬c = zc40 where sa = ZChain.supf (pzc (ob<x lim a<x)) a m = omax a sa -- x is limit ordinal, so we have sa o< m o< x @@ -1259,7 +1267,7 @@ osuc ( osuc a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x)) ⟩ x ∎ ) where open o≤-Reasoning O ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x - sam = ZChain.supf (pzc (ob<x lim m<x)) a + sam = ZChain.supf (pzc (ob<x lim m<x)) a zc42 : osuc a o≤ osuc m zc42 = osucc (o<→≤ ( omax-x _ _ ) ) sam<m : sam o< m @@ -1270,29 +1278,29 @@ zcm = ZChain.cfcs (pzc (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm zc40 : odef (UnionCF A f ay supf1 b) w zc40 with ZChain.cfcs (pzc (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm - ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ + ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where - supfb = ZChain.supf (pzc (ob<x lim b<x)) - sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a + supfb = ZChain.supf (pzc (ob<x lim b<x)) + sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a sb=sa {a} a<b = trans (sf1=sf (ordtrans<-≤ a<b b≤x)) (zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ <-osuc) ) fcb : FClosure A f (supfb a) w - fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc + fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc -- supfb a o< b assures it is in Union b zcb : odef (UnionCF A f ay supfb b) w zcb = ZChain.cfcs (pzc (ob<x lim b<x)) a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb zc40 : odef (UnionCF A f ay supf1 b) w zc40 with zcb - ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ + ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b sup=u {b} ab b≤x is-sup with osuc-≡< b≤x ... | case1 b=x = ? where zc31 : spu o≤ b - zc31 = MinSUP.minsup usup ab zc32 where - zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b) + zc31 = MinSUP.minsup usup ab zc32 where + zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b) zc32 = ? ... | case2 b<x = trans (sf1=sf ?) (ZChain.sup=u (pzc (ob<x lim b<x)) ab ? ? ) ---