Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 830:507f6582c31d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Aug 2022 07:39:18 +0900 |
| parents | 4822758b8bf8 |
| children | b91681b604d8 |
| files | src/OD.agda src/OrdUtil.agda src/zorn.agda |
| diffstat | 3 files changed, 83 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OD.agda Fri Aug 19 10:08:14 2022 +0900 +++ b/src/OD.agda Mon Aug 22 07:39:18 2022 +0900 @@ -120,7 +120,7 @@ -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD ¬OD-order : ( & : OD → Ordinal ) → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥ -¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) +¬OD-order & * c<→o< = o≤> <-osuc (c<→o< {Ords} OneObj ) -- Open supreme upper bound leads a contradition, so we use domain restriction on sup ¬open-sup : ( sup-o : (Ordinal → Ordinal ) → Ordinal) → ((ψ : Ordinal → Ordinal ) → (x : Ordinal) → ψ x o< sup-o ψ ) → ⊥
--- a/src/OrdUtil.agda Fri Aug 19 10:08:14 2022 +0900 +++ b/src/OrdUtil.agda Mon Aug 22 07:39:18 2022 +0900 @@ -35,10 +35,10 @@ o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl -osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥ -osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox -osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y -osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x +o≤> : { x y : Ordinal } → y o< osuc x → x o< y → ⊥ +o≤> {x} {y} y<ox x<y with osuc-≡< y<ox +o≤> {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y +o≤> {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x open _∧_ @@ -207,7 +207,7 @@ o≤? x y with trio< x y ... | tri< a ¬b ¬c = yes (ordtrans a <-osuc) ... | tri≈ ¬a b ¬c = yes (o≤-refl0 b) -... | tri> ¬a ¬b c = no (λ n → osuc-< n c ) +... | tri> ¬a ¬b c = no (λ n → o≤> n c ) o¬≤→< : {x z : Ordinal} → ¬ (x o< osuc z) → z o< x o¬≤→< {x} {z} not with trio< z x
--- a/src/zorn.agda Fri Aug 19 10:08:14 2022 +0900 +++ b/src/zorn.agda Mon Aug 22 07:39:18 2022 +0900 @@ -304,16 +304,14 @@ ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) )) ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt ) - order : {b s z1 : Ordinal} → b o< z → 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 - zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 - zc01 (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where + csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 + csupf-fc {b} {s} {z1} b≤<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where s<b : s o< b s<b = supf-inject ss<sb - s<z : s o< z - s<z = ordtrans s<b b<z + s≤<z : s o≤ z + s≤<z = ordtrans s<b b≤<z zc04 : odef (UnionCF A f mf ay supf (supf s)) (supf s) - zc04 = csupf (o<→≤ s<z ) + zc04 = csupf s≤<z zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ @@ -330,13 +328,15 @@ ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb ) ... | case2 lt = o<→≤ (supf-inject lt ) ... | case2 lt = o<→≤ (ordtrans (supf-inject lt) s<b) - zc01 (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where + csupf-fc {b} {s} {z1} b<z ss<sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where 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 (zc01 fc ) + 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) ⟫ + order : {b s z1 : Ordinal} → b o< z → 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 ≡ SUP.sup (sup b<z )) ∨ ( * z1 < SUP.sup ( sup b<z ) ) - zc00 = SUP.x<sup (sup b<z) (zc01 fc ) + zc00 = SUP.x<sup (sup b<z) (csupf-fc (o<→≤ b<z) ss<sb fc ) zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) zc04 with zc00 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup b<z) ) (cong (&) eq) ) @@ -669,7 +669,7 @@ zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt pchain : HOD - pchain = UnionCF A f mf ay (ZChain.supf zc) x + pchain = UnionCF A f mf ay (ZChain.supf zc) px ptotal : IsTotalOrderSet pchain ptotal {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) ) @@ -690,14 +690,14 @@ supf0 = ZChain.supf zc - sup1 : SUP A (UnionCF A f mf ay supf0 x) + sup1 : SUP A (UnionCF A f mf ay supf0 px) sup1 = supP pchain pchain⊆A ptotal sp1 = & (SUP.sup sup1 ) supf1 : Ordinal → Ordinal supf1 z with trio< z px ... | tri< a ¬b ¬c = ZChain.supf zc z - ... | tri≈ ¬a b ¬c = sp1 -- ZChain.supf zc z - ... | tri> ¬a ¬b c = sp1 -- ZChain.supf zc px + ... | tri≈ ¬a b ¬c = sp1 + ... | tri> ¬a ¬b c = sp1 pchain1 : HOD pchain1 = UnionCF A f mf ay supf1 x @@ -717,6 +717,34 @@ uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) + zc64 : {z : Ordinal } → z o< px → odef (UnionCF A f mf ay supf0 px) (supf0 z) + zc64 {z} z<px = chain-mono f mf ay supf0 zc72 zc70 where + zc70 : odef (UnionCF A f mf ay supf0 (supf0 z) ) (supf0 z) + zc70 = ZChain.csupf zc (o<→≤ z<px ) + zc71 : supf0 z o≤ supf0 px + zc71 = ZChain.supf-mono zc (o<→≤ z<px ) + zc72 : supf0 z o≤ px + zc72 = ? + zc73 : odef (UnionCF A f mf ay supf0 px ) (supf0 z) + zc73 = subst (λ k → odef (UnionCF A f mf ay supf0 px ) k ) &iso ( ZChain.csupf-fc zc o≤-refl ? (init (proj1 zc70) refl) ) + + supf1<sp1 : {z : Ordinal } → supf1 z o≤ sp1 + supf1<sp1 {z} with trio< z px | inspect supf1 z + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = o≤-refl + ... | tri> ¬a ¬b c | record { eq = eq1 } = o≤-refl + ... | tri< a ¬b ¬c | record { eq = eq1 } with trio< (supf1 z) sp1 + ... | tri< a₁ ¬b₁ ¬c₁ = subst (λ k → k o≤ sp1) eq1 (o<→≤ a₁) + ... | tri≈ ¬a b ¬c₁ = o≤-refl0 (trans (sym eq1) b ) + ... | tri> ¬a ¬b₁ c = ? where + zc65 : sp1 o< ZChain.supf zc z + zc65 = subst (λ k → sp1 o< k ) eq1 c + zc66 : ( * (ZChain.supf zc z) ≡ * sp1) ∨ (ZChain.supf zc z << sp1) + zc66 = subst₂ (λ j k → ( j ≡ k) ∨ ( j < k ) ) refl (sym *iso) zc68 where + zc68 : ( *( ZChain.supf zc z) ≡ SUP.sup sup1 ) ∨ ( * (ZChain.supf zc z) < SUP.sup sup1 ) + zc68 = SUP.x<sup sup1 (subst (λ k → odef (UnionCF A f mf ay supf0 px) k ) (sym &iso) (zc64 a) ) + zc67 : ZChain.supf zc sp1 ≡ sp1 + zc67 = ? + -- if previous chain satisfies maximality, we caan reuse it -- -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x @@ -732,25 +760,27 @@ zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w zc60 (init asp refl) with trio< u1 px | inspect supf1 u1 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) - order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 → + order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) order {s} {z2} s<u1 fc with trio< s px - ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) - ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? ? ) - ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px + ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup zc61 fc ) where + zc61 : supf0 s o< supf0 u1 + zc61 = subst (λ k → supf0 s o< k ) eq1 s<u1 + ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> supf1<sp1 s<u1 ) + ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s {!!} )) -- px o< s < u1 < px ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 ? } (init (subst (λ k → odef A k ) (sym eq1) ? ) ? ) ⟫ where + record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 {!!} } (init (subst (λ k → odef A k ) (sym eq1) {!!} ) {!!} ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) - fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ? -- ( ChainP.fcy<sup u1-is-sup fc ) - order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 → + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) {!!} -- ( ChainP.fcy<sup u1-is-sup fc ) + order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u1 → FClosure A f (supf1 s) z2 → (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) order {s} {z2} s<u1 fc with trio< s px - ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc ) - ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc ) - ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px + ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) {!!} + ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) {!!} -- ( ChainP.order u1-is-sup s<u1 fc ) + ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b {!!} ) )) -- px o< s < u1 = px ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x (o<→≤ z0<px)) ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) @@ -758,8 +788,8 @@ ... | ⟪ 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₁) ⟫ no-extension : ¬ xSUP → ZChain A f mf ay x - no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; supf-mono = ? - ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = ? + no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; supf-mono = {!!} + ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = {!!} ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o< x → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1 UnionCFR⊆ {z0} {z1} z0≤1 z0<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ @@ -767,24 +797,24 @@ zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w zc60 {w} (init asp refl) with trio< u1 px | inspect supf1 u1 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init asp refl ) ⟫ where + record { fcy<sup = fcy<sup ; order = {!!} ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init asp refl ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s - ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) - ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) ? )) + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) {!!} )) ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans (sym ? ) (ChainP.supu=u u1-is-sup) } (init ? ? ) ⟫ where + record { fcy<sup = fcy<sup ; order = {!!} ; supu=u = trans (sym {!!} ) (ChainP.supu=u u1-is-sup) } (init {!!} {!!} ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) - fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc ) + fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) {!!} ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s - ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ?( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) - ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) ? )) + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) {!!}( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) {!!} ( ChainP.order u1-is-sup {!!} (subst (λ k → FClosure A f k z2) (sym eq2) {!!} )) ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) ) @@ -802,13 +832,13 @@ ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z<x ) ( ZChain.sup zc a ) ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1) - zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x lt ) + zc61 {w} lt = ? -- SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x lt ) ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 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 (UnionCF⊆ o≤-refl a lt) } - ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } + ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where zc30 : x ≡ b zc30 with osuc-≡< b≤x @@ -816,16 +846,16 @@ ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) zcsup : xSUP zcsup with zc30 - ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) ? lt) } } + ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) {!!} lt) } } csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) csupf {b} b<x with trio< b px | inspect supf1 b - ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a ? - ... | tri≈ ¬a refl ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl ) - ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? -- UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) + ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a {!!} + ... | tri≈ ¬a refl ¬c | _ = {!!} -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl ) + ... | tri> ¬a ¬b px<b | record { eq = eq1 } = {!!} -- UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x)) sis {z} z<x with trio< z px ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc a - ... | tri≈ ¬a b ¬c = ? + ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) @@ -835,7 +865,7 @@ ... | 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 = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; sup=u = {!!} ; supf-mono = ? + record { supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} } where supx : SUP A (UnionCF A f mf ay supf0 x) supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } @@ -933,8 +963,8 @@ no-extension : ¬ xSUP → ZChain A f mf ay x no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = sup=u - ; sup = sup ; supf-is-sup = sis ; supf-mono = ? - ; csupf = ? ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where + ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} + ; csupf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x @@ -973,9 +1003,9 @@ zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) zc9 = {!!} zc8 : odef (UnionCF A f mf ay (supfu a) z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) - zc8 = ? -- ZChain.csupf (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc ) + zc8 = {!!} -- ZChain.csupf (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc ) ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z ? )) + ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z {!!} )) zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) @@ -985,7 +1015,7 @@ ... | case1 pr = no-extension {!!} ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!} ; supf = supf1 ; sup=u = {!!} - ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = ? + ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!} ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} } -- where -- x is a sup of (zc ?) ... | case2 ¬x=sup = no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention