Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 857:266e0b9027cd
supf-max
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 07 Sep 2022 21:28:30 +0900 |
| parents | d54487b6d43a |
| children | bba4ce6d2766 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 70 insertions(+), 165 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Sep 06 10:25:49 2022 +0900 +++ b/src/zorn.agda Wed Sep 07 21:28:30 2022 +0900 @@ -293,11 +293,13 @@ f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-total : IsTotalOrderSet chain + supf-max : {x : Ordinal } → z o≤ x → supf z ≡ supf x sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) + supf-inject : {x y : Ordinal } → supf x o< supf y → x o< y supf-inject {x} {y} sx<sy with trio< x y ... | tri< a ¬b ¬c = a @@ -738,19 +740,13 @@ supf0 = ZChain.supf zc - supf1 : (px z : Ordinal) → Ordinal - supf1 px z with trio< z px - ... | tri< a ¬b ¬c = ZChain.supf zc z - ... | tri≈ ¬a b ¬c = ZChain.supf zc z - ... | tri> ¬a ¬b c = ZChain.supf zc px - pchain1 : HOD - pchain1 = UnionCF A f mf ay (supf1 px) x + pchain1 = UnionCF A f mf ay supf0 x ptotal1 : IsTotalOrderSet pchain1 ptotal1 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) - uz01 = chain-total A f mf ay (supf1 px) ( (proj2 ca)) ( (proj2 cb)) + uz01 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb)) pchain⊆A1 : {y : Ordinal} → odef pchain1 y → odef A y pchain⊆A1 {y} ny = proj1 ny pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a) @@ -760,99 +756,54 @@ pinit1 {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 - zc7 : y <= supf1 px u + zc7 : y <= supf0 u zc7 = ChainP.fcy<sup is-sup (init ay refl) pcy1 : odef pchain1 y pcy1 = ⟪ ay , ch-init (init ay refl) ⟫ - supf0=1 : {px z : Ordinal } → z o≤ px → supf0 z ≡ supf1 px z - supf0=1 {px} {z} z≤px with trio< z px - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c ) + supfx : {z : Ordinal } → x o≤ z → supf0 px ≡ supf0 z + supfx {z} x≤z with trio< z px + ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc ))) + ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op))) + ... | tri> ¬a ¬b c = ZChain.supf-max zc (o<→≤ c) - supfx : {z : Ordinal } → z ≡ x → supf0 px ≡ supf1 px z - supfx {z} z=x with trio< z px - ... | tri< a ¬b ¬c = ⊥-elim ( o<¬≡ z=x (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc ))) - ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ z=x (subst (λ k → k o< x ) (sym b) (pxo<x op))) - ... | tri> ¬a ¬b c = refl - - supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 px b) + supf∈A : {b : Ordinal} → b o≤ x → odef A (supf0 b) supf∈A {b} b≤z with trio< b px ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a )) ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b )) - ... | tri> ¬a ¬b c = proj1 ( ZChain.csupf zc o≤-refl ) - - supf-mono : {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b - supf-mono = ? - - fc0→1 : {px s z : Ordinal } → s o≤ px → FClosure A f (supf0 s) z → FClosure A f (supf1 px s) z - fc0→1 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc - - fc1→0 : {px s z : Ordinal } → s o≤ px → FClosure A f (supf1 px s) z → FClosure A f (supf0 s) z - fc1→0 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc + ... | tri> ¬a ¬b c = subst (λ k → odef A k ) (ZChain.supf-max zc (o<→≤ c)) (proj1 ( ZChain.csupf zc o≤-refl)) - CP0→1 : {px u : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) - → u o≤ px → ChainP A f mf ay supf0 u → ChainP A f mf ay (supf1 px) u - CP0→1 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where - fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u ) - fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (supf0=1 u≤px) ( ChainP.fcy<sup cp fc ) - order : {s : Ordinal} {z2 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z2 → - (z2 ≡ supf1 px u) ∨ (z2 << supf1 px u) - order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (supf0=1 u≤px) ( ChainP.order cp ss<su (fc1→0 s≤px fc )) where - s≤px : s o≤ px - s≤px = ordtrans (supf-inject0 supf-mono s<u) u≤px - ss<su : supf0 s o< supf0 u - ss<su = subst₂ (λ j k → j o< k ) (sym (supf0=1 s≤px )) (sym (supf0=1 u≤px)) s<u + supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b + supf-mono = ZChain.supf-mono zc - CP1→0 : {px u : Ordinal } → ( {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) - → u o≤ px → ChainP A f mf ay (supf1 px) u → ChainP A f mf ay supf0 u - CP1→0 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where - fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u ) - fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym (supf0=1 u≤px)) ( ChainP.fcy<sup cp fc ) - order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z2 → - (z2 ≡ supf0 u) ∨ (z2 << supf0 u) - order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym (supf0=1 u≤px)) ( ChainP.order cp ss<su (fc0→1 s≤px fc )) where - s≤px : s o≤ px - s≤px = ordtrans (supf-inject0 (ZChain.supf-mono zc) s<u) u≤px - ss<su : supf1 px s o< supf1 px u - ss<su = subst₂ (λ j k → j o< k ) (supf0=1 s≤px ) (supf0=1 u≤px) s<u - - UnionCF0⊆1 : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px → UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay (supf1 px) z - UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = - ⟪ au , ch-is-sup u u≤z (CP0→1 supf-mono (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫ - - UnionCF1⊆0 : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px → UnionCF A f mf ay (supf1 px) z ⊆' UnionCF A f mf ay supf0 z - UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = - ⟪ au , ch-is-sup u u≤z (CP1→0 supf-mono (OrdTrans u≤z z≤px ) is-sup) - (fc1→0 (OrdTrans u≤z z≤px ) fc) ⟫ - - -- zc100 : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1 - -- zc100 = ? + supf-max : {z : Ordinal} → x o≤ z → supf0 x ≡ supf0 z + supf-max {z} z≤x = trans ( sym zc02) zc01 where + zc02 : supf0 px ≡ supf0 x + zc02 = ZChain.supf-max zc (o<→≤ (pxo<x op)) + zc01 : supf0 px ≡ supf0 z + zc01 = ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x) -- if previous chain satisfies maximality, we caan reuse it -- -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x no-extension : ¬ xSUP (UnionCF A f mf ay supf0 px) x → ZChain A f mf ay x - no-extension ¬sp=x = record { supf = supf1 px ; sup = sup ; supf-mono = supf-mono - ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf + no-extension ¬sp=x = record { supf = supf0 ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = supf-max + ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where pchain0=1 : pchain ≡ pchain1 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 u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 supf-mono u1≤x u1-is-sup) (fc0→1 u1≤x fc) ⟫ + zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) u1-is-sup fc ⟫ 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 u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x - ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 supf-mono u1≤px u1-is-sup) (fc1→0 u1≤px fc) ⟫ where + ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px u1-is-sup fc ⟫ where u1≤px : u1 o≤ px u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt) ... | case1 eq = ⊥-elim (¬sp=x zcsup) where - s1u=x : supf1 px u1 ≡ x + s1u=x : supf0 u1 ≡ x s1u=x = trans (ChainP.supu=u u1-is-sup) eq zc13 : osuc px o< osuc u1 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq) ) @@ -864,32 +815,40 @@ zc14 : u ≡ osuc px zc14 = begin u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ - supf0 u ≡⟨ supf0=1 u≤x ⟩ - supf1 px u ≡⟨ eq1 ⟩ - supf1 px u1 ≡⟨ s1u=x ⟩ + supf0 u ≡⟨ eq1 ⟩ + supf0 u1 ≡⟨ s1u=x ⟩ x ≡⟨ sym (Oprev.oprev=x op) ⟩ osuc px ∎ where open ≡-Reasoning - ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt (fc0→1 u≤x fc) ) - zc12 : supf1 px x ≡ u1 - zc12 = subst (λ k → supf1 px k ≡ u1) eq (ChainP.supu=u u1-is-sup) + ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt fc ) + zc12 : supf0 x ≡ u1 + zc12 = subst (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup) zcsup : xSUP (UnionCF A f mf ay supf0 px) x zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) ; is-sup = record { x<sup = x<sup } } - sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay (supf1 px) z) - sup {z} z≤x with trio< z px | inspect (supf1 px) z - ... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o<→≤ a)) (ZChain.sup zc (o<→≤ a) ) - ... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) ) - ... | tri> ¬a ¬b px<z | record { eq = eq1} = subst (λ k → SUP A k ) - (trans pchain0=1 (cong (λ k → UnionCF A f mf ay (supf1 px) k ) (sym zc30) )) (ZChain.sup zc o≤-refl ) where + record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where + field + tsup : SUP A (UnionCF A f mf ay supf0 z) + tsup=sup : supf0 z ≡ & (SUP.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 = ZChain.sup zc (o<→≤ a) ; tsup=sup = ZChain.supf-is-sup zc (o<→≤ a) } + ... | tri≈ ¬a b ¬c = record { tsup = ZChain.sup zc (o≤-refl0 b) ; tsup=sup = ZChain.supf-is-sup zc (o≤-refl0 b) } + ... | tri> ¬a ¬b px<z = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 } ; tsup=sup = zc33 } where + zc32 = ZChain.sup zc o≤-refl zc30 : z ≡ x zc30 with osuc-≡< z≤x ... | case1 eq = eq ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) + zc34 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) + zc34 {w} lt = SUP.x<sup zc32 (subst (λ k → odef k (& w)) (sym pchain0=1) + (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt )) + zc33 : supf0 z ≡ & (SUP.sup zc32) + zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) sup=u : {b : Ordinal} (ab : odef A b) → - b o≤ x → IsSup A (UnionCF A f mf ay (supf1 px) b) ab → (supf1 px) b ≡ b + b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab → supf0 b ≡ b sup=u {b} ab b≤x is-sup with trio< b px - ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o<→≤ a) lt) } - ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o≤-refl0 b) lt) } + ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup lt } + ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup lt } ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where zc30 : x ≡ b zc30 with osuc-≡< b≤x @@ -899,80 +858,21 @@ zcsup with zc30 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt) } } - csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b) - csupf {b} b≤x = zc05 where - zc04 : (b o≤ px ) ∨ (b ≡ x ) - zc04 with trio< b px - ... | tri< a ¬b ¬c = case1 (o<→≤ a) - ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b) - ... | tri> ¬a ¬b px<b with osuc-≡< b≤x - ... | 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 ⟫ ) - zc05 : odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b) - zc05 with zc04 - ... | case2 b=x with ZChain.csupf zc o≤-refl - ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supfx b=x) au - , ch-init (subst₂ (λ j k → FClosure A f j k ) refl (supfx b=x) fc) ⟫ - ... | ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (supfx b=x) au - , ch-is-sup u (subst (λ k → u o≤ k) (supfx b=x) u≤x) zc13 zc06 ⟫ where - zc13 : ChainP A f mf ay (supf1 px) u - zc13 with trio< u px - ... | tri< a ¬b ¬c = CP0→1 supf-mono (o<→≤ a) is-sup - ... | tri≈ ¬a b ¬c = CP0→1 supf-mono (o≤-refl0 b) is-sup - ... | tri> ¬a ¬b px<u = ? - zc08 : supf0 u o≤ supf0 px - zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x - zc06 : FClosure A f (supf1 px u) (supf1 px b) - zc06 with osuc-≡< zc08 - ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supfx b=x) fc where - zc10 : supf0 u ≡ supf1 px u - zc10 with trio< u px - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b px<u = eq - ... | case2 lt = subst₂ (λ j k → FClosure A f j k ) (supf0=1 (o<→≤ zc09)) (supfx b=x) fc where - zc09 : u o< px - zc09 = supf-inject0 (ZChain.supf-mono zc) lt - zc07 : FClosure A f (supf0 u) (supf0 px) - zc07 = fc - zc05 | case1 b≤px with ZChain.csupf zc b≤px - ... | ⟪ au , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au - , ch-init (subst₂ (λ j k → FClosure A f j k ) refl (supf0=1 b≤px) fc) ⟫ - ... | ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (supf0=1 b≤px) au - , ch-is-sup u (subst (λ k → u o≤ k) (supf0=1 b≤px) u≤x) zc13 zc06 ⟫ where - zc13 : ChainP A f mf ay (supf1 px) u - zc13 with trio< u px - ... | tri< a ¬b ¬c = CP0→1 supf-mono (o<→≤ a) is-sup - ... | tri≈ ¬a b ¬c = CP0→1 supf-mono (o≤-refl0 b) is-sup - ... | tri> ¬a ¬b px<u = ? - zc08 : supf0 u o≤ supf0 b - zc08 = subst₂ (λ j k → j o≤ k) (sym (ChainP.supu=u is-sup)) refl u≤x - zc06 : FClosure A f (supf1 px u) (supf1 px b) - zc06 with osuc-≡< zc08 - ... | case1 eq = subst₂ (λ j k → FClosure A f j k ) zc10 (supf0=1 b≤px) fc where - zc10 : supf0 u ≡ supf1 px u - zc10 with trio< u px - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b px<u = zc12 where - zc11 : supf0 u o≤ supf0 px - zc11 = subst (λ k → k o≤ supf0 px ) (sym eq) ( ZChain.supf-mono zc b≤px ) - zc12 : supf0 u ≡ supf0 px - zc12 with osuc-≡< zc11 - ... | case1 eq2 = eq2 - ... | case2 lt = ⊥-elim ( o<> px<u (ZChain.supf-inject zc lt )) - ... | case2 lt = subst₂ (λ j k → FClosure A f j k ) (supf0=1 zc09) (supf0=1 b≤px) fc where - zc09 : u o≤ px - zc09 = ordtrans (supf-inject0 (ZChain.supf-mono zc) lt) b≤px - zc07 : FClosure A f (supf0 u) (supf0 b) - zc07 = fc - sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 px z ≡ & (SUP.sup (sup z≤x)) - sis {z} z≤x = zc40 where - zc40 : supf1 px z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error - zc40 with trio< z px | inspect (supf1 px) z | inspect sup z≤x - ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? - ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? - ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ? + + zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x ) + zc04 {b} b≤x with trio< b px + ... | tri< a ¬b ¬c = case1 (o<→≤ a) + ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b) + ... | tri> ¬a ¬b px<b with osuc-≡< b≤x + ... | 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 ⟫ ) + + csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b) + csupf {b} b≤x with zc04 b≤x + ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) (ZChain.supf-max zc zc05 ) ( ZChain.csupf zc o≤-refl ) where + zc05 : px o≤ b + zc05 = subst (λ k → px o≤ k) (sym b=x) (o<→≤ (pxo<x op) ) + ... | case1 b≤px = ZChain.csupf zc b≤px zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) @@ -982,15 +882,20 @@ ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) ... | case1 is-sup = -- x is a sup of zc - record { supf = supf1 x ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!} + record { supf = ? ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} } where + supf1 : Ordinal → Ordinal + supf1 z with trio< z px + ... | tri< a ¬b ¬c = ZChain.supf zc z + ... | tri≈ ¬a b ¬c = ZChain.supf zc z + ... | tri> ¬a ¬b c = x supx : SUP A (UnionCF A f mf ay supf0 x) supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } spx = & (SUP.sup supx ) x=spx : x ≡ spx x=spx = sym &iso psupf1 : Ordinal → Ordinal - psupf1 z = supf1 x z + psupf1 z = ? csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b) csupf {b} b≤x with trio< b px | inspect psupf1 b ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫