Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 800:06eedb0d26a0
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Aug 2022 14:20:26 +0900 |
| parents | c8a166abcae0 |
| children | 8373b130ba41 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 112 insertions(+), 121 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Aug 07 18:39:18 2022 +0900 +++ b/src/zorn.agda Mon Aug 08 14:20:26 2022 +0900 @@ -124,28 +124,89 @@ ... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx ) ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx ) +fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ +fcn s mf (init as refl) = zero +fcn {A} s {x} {f} mf (fsuc y p) with proj1 (mf y (A∋fc s f mf p)) +... | case1 eq = fcn s mf p +... | case2 y<fy = suc (fcn s mf p ) + +fcn-inject : {A : HOD} (s : Ordinal) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) + → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx ≡ fcn s mf cy → * x ≡ * y +fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where + fc06 : {y : Ordinal } { as : odef A s } (eq : s ≡ y ) { j : ℕ } → ¬ suc j ≡ fcn {A} s {y} {f} mf (init as eq ) + fc06 {x} {y} refl {j} not = fc08 not where + fc08 : {j : ℕ} → ¬ suc j ≡ 0 + fc08 () + fc07 : {x : Ordinal } (cx : FClosure A f s x ) → 0 ≡ fcn s mf cx → * s ≡ * x + fc07 {x} (init as refl) eq = refl + fc07 {.(f x)} (fsuc x cx) eq with proj1 (mf x (A∋fc s f mf cx ) ) + ... | case1 x=fx = subst (λ k → * s ≡ k ) x=fx ( fc07 cx eq ) + -- ... | case2 x<fx = ? + fc00 : (i j : ℕ ) → i ≡ j → {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx → j ≡ fcn s mf cy → * x ≡ * y + fc00 (suc i) (suc j) x cx (init x₃ x₄) x₁ x₂ = ⊥-elim ( fc06 x₄ x₂ ) + fc00 (suc i) (suc j) x (init x₃ x₄) (fsuc x₅ cy) x₁ x₂ = ⊥-elim ( fc06 x₄ x₁ ) + fc00 zero zero refl (init _ refl) (init x₁ refl) i=x i=y = refl + fc00 zero zero refl (init as refl) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) ) + ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy (fc07 cy i=y) -- ( fc00 zero zero refl (init as refl) cy i=x i=y ) + fc00 zero zero refl (fsuc x cx) (init as refl) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) + ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx (sym (fc07 cx i=x)) -- ( fc00 zero zero refl cx (init as refl) i=x i=y ) + fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) + ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy i=x i=y ) + fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) ) + ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) (suc j) i=j cx cy i=x j=y ) + ... | case1 x=fx | case2 y<fy = subst (λ k → k ≡ * (f y)) x=fx (fc02 x cx i=x) where + fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) → suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y) + fc02 x1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x) + fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) ) + ... | case1 eq = trans (sym eq) ( fc02 x1 cx1 i=x1 ) -- derefence while f x ≡ x + ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where + fc04 : * x1 ≡ * y + fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y) + ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ k ) y=fy (fc03 y cy j=y) where + 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 ) 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) + ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y))) + + +fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) + → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy → * x < * y +fcn-< {A} s {x} {y} {f} mf cx cy x<y = fc01 (fcn s mf cy) cx cy refl x<y where + fc06 : {y : Ordinal } { as : odef A s } (eq : s ≡ y ) { j : ℕ } → ¬ suc j ≡ fcn {A} s {y} {f} mf (init as eq ) + fc06 {x} {y} refl {j} not = fc08 not where + fc08 : {j : ℕ} → ¬ suc j ≡ 0 + fc08 () + fc01 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → fcn s mf cx Data.Nat.< i → * x < * y + fc01 (suc i) cx (init x₁ x₂) x (s≤s x₃) = ⊥-elim (fc06 x₂ x) + fc01 (suc i) {y} cx (fsuc y1 cy) i=y (s≤s x<i) with proj1 (mf y1 (A∋fc s f mf cy ) ) + ... | case1 y=fy = subst (λ k → * x < k ) y=fy ( fc01 (suc i) {y1} cx cy i=y (s≤s x<i) ) + ... | case2 y<fy with <-cmp (fcn s mf cx ) i + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i c ) + ... | tri≈ ¬a b ¬c = subst (λ k → k < * (f y1) ) (fcn-inject s mf cy cx (sym (trans b (cong pred i=y) ))) y<fy + ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO fc02 y<fy where + fc03 : suc i ≡ suc (fcn s mf cy) → i ≡ fcn s mf cy + fc03 eq = cong pred eq + fc02 : * x < * y1 + fc02 = fc01 i cx cy (fc03 i=y ) a + fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x ) -fcn-cmp-1 : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) - → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → * x < * y → (* (f x) ≡ * y) ∨ ( * (f x) < * y ) -fcn-cmp-1 {A} s f mf (init x refl) (init x₁ refl) x<y = {!!} -fcn-cmp-1 {A} s f mf (init x refl) (fsuc x₁ cy) x<y = {!!} -fcn-cmp-1 {A} s f mf (fsuc x cx) (init ay refl) x<y = {!!} -fcn-cmp-1 {A} s f mf (fsuc x cx) (fsuc y cy) x<y with proj1 (mf x (A∋fc s f mf cx)) | proj1 (mf y (A∋fc s f mf cy)) -... | case1 eqx | case1 eqy = {!!} -... | case1 eqx | case2 lt = {!!} -... | case2 lt | case1 eqy = {!!} -... | case2 ltx | case2 lty = {!!} +fcn-cmp {A} s {x} {y} f mf cx cy with <-cmp ( fcn s mf cx ) (fcn s mf cy ) +... | tri< a ¬b ¬c = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where + fc11 : * x < * y + fc11 = fcn-< {A} s {x} {y} {f} mf cx cy a +... | tri≈ ¬a b ¬c = tri≈ (λ lt → <-irr (case1 (sym fc10)) lt) fc10 (λ lt → <-irr (case1 fc10) lt) where + fc10 : * x ≡ * y + fc10 = fcn-inject {A} s {x} {y} {f} mf cx cy b +... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12 where + fc12 : * y < * x + fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c -fcn-cmp {A} s {.s} {y} f mf (init ax refl) (init ay refl) = {!!} -fcn-cmp {A} s {.s} {.(f x)} f mf (init ax refl) (fsuc x cy) = {!!} -fcn-cmp {A} s {.(f x)} {y} f mf (fsuc x cx) (init ay refl) = {!!} -fcn-cmp {A} s {.(f x)} {.(f y)} f mf (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx)) | proj1 (mf y (A∋fc s f mf cy)) -... | case1 eqx | case1 eqy = {!!} -... | case1 eqx | case2 lt = {!!} -... | case2 lt | case1 eqy = {!!} -... | case2 ltx | case2 lty = {!!} -- open import Relation.Binary.Properties.Poset as Poset @@ -190,7 +251,7 @@ record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where field fcy<sup : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) - order : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) + order : {s z1 : Ordinal} → (lt : s o< u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) supu=u : supf u ≡ u -- Union of supf z which o< x @@ -235,62 +296,11 @@ ... | 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 ) - supf-mono : {x y1 : Ordinal } → x o< y1 → supf x o≤ supf y1 - supf-mono {x} {y1} x<y1 = sf<sy1 where - -- supf x << supf y1 → supf x o< supf y1 - -- x o< y1 → supf x <= supf y1 - -- z o≤ x → supf x ≡ supf y1 ≡ supf z - -- x o< z → z o< y1 → supf x ≡ supf y1 ≡ supf z - supy : {x : Ordinal } → x o≤ z → FClosure A f y (supf x) → supf x ≡ y - supy {x} x≤z fcx = ? where - zc06 : ( * y ≡ SUP.sup (sup x≤z )) ∨ ( * y < SUP.sup ( sup x≤z ) ) - zc06 = SUP.x<sup (sup x≤z) ⟪ subst (λ k → odef A k ) (sym &iso) ay , ch-init (init ay (sym &iso) ) ⟫ - sf<sy1 : supf x o≤ supf y1 - sf<sy1 with trio< x z - ... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y1 ) <-osuc ) ) )) - ... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y1) b (o<→≤ x<y1)))) - ... | tri< x<z ¬b ¬c with trio< (supf x) (supf y1) - ... | tri< a ¬b ¬c = o<→≤ a - ... | tri≈ ¬a b ¬c = o≤-refl0 b - ... | tri> ¬a ¬b sy1<sx with trio< z y1 - ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b y1<z = ? - zc04 : x o< z → y1 o≤ z → supf x o≤ supf y1 - zc04 x<z y1≤z with csupf (o<→≤ x<z) | csupf y1≤z - ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ with fcy<sup (o<→≤ x<z) fcy1 - ... | case1 eq = o≤-refl0 (sym eq) - ... | case2 lt with fcy<sup y1≤z fcx - ... | case1 eq = o≤-refl0 eq - ... | case2 lt1 = ⊥-elim ( <-irr (case2 lt) lt1 ) - zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ with fcy<sup (o<→≤ x<z) fcy1 - ... | case1 eq = o≤-refl0 (sym eq) - ... | case2 lt with trio< (supf x) (supf y1) - ... | tri< a ¬b ¬c = o<→≤ a - ... | tri≈ ¬a b ¬c = o≤-refl0 b - ... | tri> ¬a ¬b y1<z = ? where - zc05 : ( supf y1 ≡ supf ux ) ∨ (supf y1 << supf ux ) - zc05 = ChainP.fcy<sup is-sup-x fcy1 - zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ | case2 lt1 = ? -- sy1 << sx - zc04 x<z y1≤z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-is-sup uy1 uy1≤z is-sup-y1 fcy1 ⟫ = ? - zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-is-sup uy1 uy1≤z is-sup-y1 fcy1 ⟫ = ? - -- ... | tri< a ¬b ¬c = csupf (o<→≤ a) - -- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b) - -- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay1 supf x) k ) ? (csupf ? ) - -- csy1 : odef (UnionCF A f mf ay1 supf y1) (supf y1) - -- csy1 = csupf ? - 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 sf<sb fc = zc04 where + order : {b s z1 : Ordinal} → b o< z → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) + order {b} {s} {z1} b<z s<b 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) zc03 where - s<b : s o< b - s<b with trio< s b - ... | tri< a ¬b ¬c = a - ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (cong supf b) sf<sb ) - ... | tri> ¬a ¬b c with osuc-≡< ( supf-mono c ) - ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sf<sb ) - ... | case2 lt = ⊥-elim ( o<> lt sf<sb ) s<z : s o< z s<z = ordtrans s<b b<z zc03 : odef (UnionCF A f mf ay supf b) (supf s) @@ -360,7 +370,7 @@ ct01 with s≤fc (supf ua) f mf fca ... | case1 eq = subst (λ k → * b < k ) eq ct00 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt - ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< (supf ua) (supf ub) + ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub ... | tri< a₁ ¬b ¬c with ChainP.order supb a₁ 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 @@ -377,7 +387,7 @@ ... | case1 eq = subst (λ k → * a < k ) eq ct03 ... | case2 lt = IsStrictPartialOrder.trans POO ct03 lt ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri≈ ¬a eq ¬c - = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (sym eq) fcb ) + = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb ) ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa c 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 @@ -503,11 +513,13 @@ record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz ) } ) m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz - m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) + m09 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz + m10 : {y₁ : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) y₁ → (y₁ ≡ b) ∨ (y₁ << b) + m10 = {!!} m06 : ChainP A f mf ay (ZChain.supf zc) b - m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = ZChain.sup=u zc ab b<A {!!} } + m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = ZChain.sup=u zc ab b<A record { x<sup = m10} } ... | no lim = record { is-max = is-max } where is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → b o< x → (ab : odef A b) → @@ -522,14 +534,16 @@ m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc - m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) + m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc m05 : b ≡ ZChain.supf zc b m05 = sym (ZChain.sup=u zc ab m09 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} ) -- ZChain on x + m10 : {y₁ : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) y₁ → (y₁ ≡ b) ∨ (y₁ << b) + m10 = {!!} m06 : ChainP A f mf ay (ZChain.supf zc) b - m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = ZChain.sup=u zc ab m09 {!!} } + m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = ZChain.sup=u zc ab m09 record { x<sup = m10 } } --- --- the maximum chain has fix point of any ≤-monotonic function @@ -610,7 +624,7 @@ initChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; sup = {!!} ; supf-is-sup = {!!} - ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; supf-mono = mono ; csupf = {!!} } where + ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; csupf = {!!} } where spi = & (SUP.sup (ysup f mf ay)) isupf : Ordinal → Ordinal isupf z = spi @@ -634,8 +648,6 @@ itotal {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 isupf (proj2 ca) (proj2 cb) - mono : {x : Ordinal} {z : Ordinal} → x o< z → isupf x o≤ isupf z - mono {x} {z} x<z = o≤-refl csupf : {z : Ordinal} → z o≤ o∅ → odef (UnionCF A f mf ay isupf z ) (isupf z) csupf {z} z≤0 = ⟪ asi , ch-is-sup o∅ o∅≤z uz02 (init asi refl) ⟫ where uz03 : {z : Ordinal } → FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi) @@ -648,7 +660,7 @@ uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi) uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi ) uz02 : ChainP A f mf ay isupf o∅ - uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = ? } + uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → {!!} ; supu=u = {!!} } SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; A∋maximal = SUP.A∋maximal sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt) } @@ -707,28 +719,28 @@ -- -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x no-extension : ¬ sp1 ≡ x → ZChain A f mf ay x - no-extension ¬sp=x = record { supf = supf1 ; supf-mono = {!!} ; sup = sup + no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; initial = {!!} ; chain∋init = {!!} ; sup=u = {!!} ; supf-is-sup = {!!} ; csupf = {!!} ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} } where UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay supf0 x - UnionCF⊆ ⟪ as , ch-init fc ⟫ = UnionCF⊆ ⟪ as , ch-init fc ⟫ + UnionCF⊆ ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1 ; supu=u = su=u1 } fc ⟫ with trio< u px ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = {!!} } fc ⟫ where - order0 : {s z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 + order0 : {s z1 : Ordinal} → s o< u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s - ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su ) + ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} {!!} (subst (λ k → FClosure A f k z1 ) (sym eq1) fc ) - ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su ) + ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} {!!} (subst (λ k → FClosure A f k z1 ) (sym eq1) fc ) ... | tri> ¬a ¬b c | record {eq = eq1} = {!!} ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = {!!}} fc ⟫ where - order0 : {s z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 + order0 : {s z1 : Ordinal} → s o< u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s - ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su ) + ... | tri< a ¬b ¬c | record {eq = eq1} = o1 {s} {z1} {!!} (subst (λ k → FClosure A f k z1 ) (sym eq1) fc ) - ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su ) + ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} {!!} (subst (λ k → FClosure A f k z1 ) (sym eq1) fc ) ... | tri> ¬a ¬b px<s | record {eq = eq1} = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x {!!} )) where s≤u : s o≤ u @@ -759,7 +771,7 @@ ... | 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 = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!} } where + ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} } where supx : SUP A (UnionCF A f mf ay supf0 x) supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } spx = & (SUP.sup supx ) @@ -837,7 +849,7 @@ no-extension : ¬ spu ≡ x → ZChain A f mf ay x no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = {!!} ; sup = sup ; supf-is-sup = sis - ; csupf = csupf ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; supf-mono = {!!} } where + ; csupf = 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 x ⊆' UnionCF A f mf ay (supfu a) x @@ -849,7 +861,7 @@ ... | tri> ¬a ¬b c = SUP⊆ {!!} usup sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z)) sis {z} z≤x with trio< z x - ... | tri< a ¬b ¬c = ? where + ... | tri< a ¬b ¬c = {!!} where zc8 = ZChain.supf-is-sup (pzc z a) o≤-refl ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c with osuc-≡< z≤x @@ -857,39 +869,18 @@ ... | case2 lt = ⊥-elim ( ¬a lt ) sup=u : {b : Ordinal} (ab : odef A b) → b o< x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b sup=u {b} ab b<x is-sup with trio< b x - ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b) (ob<x lim a)) ab <-osuc record { x<sup = ? } - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b) (ob<x lim a)) ab <-osuc record { x<sup = {!!} } + ... | tri≈ ¬a b ¬c = {!!} + ... | tri> ¬a ¬b c = {!!} csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z) csupf {z} z<x with trio< z x ... | tri< a ¬b ¬c = zc9 where zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) - zc9 = ? + 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 ) - ... | tri≈ ¬a b ¬c = ? -- ⊥-elim (¬a z<x) - ... | tri> ¬a ¬b c = ? -- ⊥-elim (¬a z<x) - supf-mono : {a b : Ordinal} → a o< b → supf1 a o≤ supf1 b - supf-mono {a0} {b0} a<b = zc10 where - -- x o≤ a → supf1 a ≡ supf1 b ≡ spu - -- x o≤ b → supf1 b ≡ spu - -- a o< x → b o≤ x → supf1 (supf1 a) ≡ supf1 a - -- supf1 (supf1 b) ≡ supf1 b - usa : odef (UnionCF A f mf ay (supfu ?) (osuc a0)) (supf1 a0) - usa = ? - usb : odef (UnionCF A f mf ay (supfu ?) (osuc b0)) (supf1 b0) - usb = ? - zc10 : supf1 a0 o≤ supf1 b0 - zc10 with trio< a0 x | trio< b0 x - ... | tri< a ¬b ¬c | tri< a' ¬b' ¬c' = ? where - zc11 = ZChain.supf-mono (pzc (osuc a0) (ob<x lim a)) a<b - zc12 = ZChain.supf-mono (pzc (osuc b0) (ob<x lim a')) a<b - ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c' = ? - ... | tri< a ¬b ¬c | tri> ¬a ¬b' c = ? - ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c' = ? - ... | tri≈ ¬a b ¬c | tri≈ ¬a' b' ¬c' = ? - ... | tri≈ ¬a b ¬c | tri> ¬a' ¬b c = ? - ... | tri> ¬a ¬b c | _ = ? + ... | tri≈ ¬a b ¬c = {!!} -- ⊥-elim (¬a z<x) + ... | tri> ¬a ¬b c = {!!} -- ⊥-elim (¬a z<x) zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) @@ -900,7 +891,7 @@ ... | 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 = {!!} - ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; supf-mono = {!!} } where -- x is a sup of (zc ?) + ; 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 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)