Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 796:171123c92007
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Aug 2022 17:57:41 +0900 |
| parents | 408e7e8a3797 |
| children | 3a8493e6cd67 |
| files | src/OrdUtil.agda src/zorn.agda |
| diffstat | 2 files changed, 56 insertions(+), 154 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OrdUtil.agda Fri Aug 05 16:21:46 2022 +0900 +++ b/src/OrdUtil.agda Fri Aug 05 17:57:41 2022 +0900 @@ -57,7 +57,7 @@ ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x ob<x {b} {x} lim b<x with trio< (osuc b) x ... | tri< a ¬b ¬c = a -... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x } ) +... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { oprev = b ; oprev=x = ob=x } ) ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ ) osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox
--- a/src/zorn.agda Fri Aug 05 16:21:46 2022 +0900 +++ b/src/zorn.agda Fri Aug 05 17:57:41 2022 +0900 @@ -124,115 +124,29 @@ ... | 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 - 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 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 ( 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 ( 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 .(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 .(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 - 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) {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 {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-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-imm : {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 ) ∧ ( * y < * (f x )) ) -fcn-imm {A} s {x} {y} f mf cx cy ⟪ x<y , y<fx ⟫ = fc21 where - fc20 : fcn s mf cy Data.Nat.< suc (fcn s mf cx) → (fcn s mf cy ≡ fcn s mf cx) ∨ ( fcn s mf cy Data.Nat.< fcn s mf cx ) - fc20 y<sx with <-cmp ( fcn s mf cy ) (fcn s mf cx ) - ... | tri< a ¬b ¬c = case2 a - ... | tri≈ ¬a b ¬c = case1 b - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> y<sx (s≤s c)) - fc17 : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → suc (fcn s mf cx) ≡ fcn s mf cy → * (f x ) ≡ * y - fc17 {x} {y} cx cy sx=y = fc18 (fcn s mf cy) cx cy refl sx=y where - fc18 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → suc (fcn s mf cx) ≡ i → * (f x) ≡ * y - fc18 (suc i) {y} cx (fsuc y1 cy) i=y sx=i with proj1 (mf y1 (A∋fc s f mf cy ) ) - ... | case1 y=fy = subst (λ k → * (f x) ≡ k ) y=fy ( fc18 (suc i) {y1} cx cy i=y sx=i) -- dereference - ... | case2 y<fy = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k) ) ) fc19) where - fc19 : * x ≡ * y1 - fc19 = fcn-inject s mf cx cy (cong pred ( trans sx=i i=y )) - fc21 : ⊥ - fc21 with <-cmp (suc ( fcn s mf cx )) (fcn s mf cy ) - ... | tri< a ¬b ¬c = <-irr (case2 y<fx) (fc22 a) where -- suc ncx < ncy - cxx : FClosure A f s (f x) - cxx = fsuc x cx - fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx)) - fc16 x (init as refl) with proj1 (mf s as ) - ... | case1 _ = case1 refl - ... | case2 _ = case2 refl - fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) ) - ... | case1 _ = case1 refl - ... | case2 _ = case2 refl - fc22 : (suc ( fcn s mf cx )) Data.Nat.< (fcn s mf cy ) → * (f x) < * y - fc22 a with fc16 x cx - ... | case1 eq = fcn-< s mf cxx cy (subst (λ k → k Data.Nat.< fcn s mf cy ) eq (<-trans a<sa a)) - ... | case2 eq = fcn-< s mf cxx cy (subst (λ k → k Data.Nat.< fcn s mf cy ) eq a ) - ... | tri≈ ¬a b ¬c = <-irr (case1 (fc17 cx cy b)) y<fx - ... | tri> ¬a ¬b c with fc20 c -- ncy < suc ncx - ... | case1 y=x = <-irr (case1 ( fcn-inject s mf cy cx y=x )) x<y - ... | case2 y<x = <-irr (case2 x<y) (fcn-< s mf cy cx y<x ) +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 = {!!} -fc-conv : (A : HOD ) (f : Ordinal → Ordinal) {b u : Ordinal } - → {p0 p1 : Ordinal → Ordinal} - → p0 u ≡ p1 u - → FClosure A f (p0 u) b → FClosure A f (p1 u) b -fc-conv A f {.(p0 u)} {u} {p0} {p1} p0u=p1u (init ap0u refl) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) - ( init (subst (λ k → odef A k) p0u=p1u ap0u ) refl) -fc-conv A f {_} {u} {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv A f {_} {u} {p0} {p1} p0u=p1u fc) -- open import Relation.Binary.Properties.Poset as Poset @@ -312,25 +226,13 @@ 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 (osuc b)) ab → supf b ≡ b supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) + csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) + supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y fcy<sup : {u w : Ordinal } → u o< z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf fcy<sup {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ 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 (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) )) ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt ) - - csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b) - csupf {b} b<z = ⟪ asb , ch-is-sup b o≤-refl is-sup (init asb refl) ⟫ where - asb : odef A (supf b) - asb = subst (λ k → odef A k ) (sym (supf-is-sup ? )) (SUP.A∋maximal (sup ? )) - is-sup : ChainP A f mf ay supf b - is-sup = record { fcy<sup = fcy<sup b<z ; order = ? ; supu=u = ? } - supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y - supf-mono = ? - -- supf-is-sup {x} x≤z = ? where - -- zc51 : * (supf x) ≡ SUP.sup (sup x≤z ) - -- zc51 = ==→o≡ record { eq→ ? ; eq← = ? } - -- zc50 : supf x ≡ & (SUP.sup (sup x<z) ) - -- zc50 = ? 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 zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 @@ -558,7 +460,7 @@ → 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 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 {!!} } ... | 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) → @@ -580,7 +482,7 @@ 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 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 {!!} } --- --- the maximum chain has fix point of any ≤-monotonic function @@ -660,8 +562,8 @@ ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) 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 = csupf } where + 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 spi = & (SUP.sup (ysup f mf ay)) isupf : Ordinal → Ordinal isupf z = spi @@ -733,7 +635,7 @@ pchain⊆A {y} ny = proj1 ny pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ - pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u ? is-sup (fsuc _ fc ) ⟫ + pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u {!!} is-sup (fsuc _ fc ) ⟫ pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ pinit {a} ⟪ aa , ua ⟫ with ua ... | ch-init fc = s≤fc y f mf fc @@ -758,13 +660,13 @@ -- -- 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 - ; initial = ? ; chain∋init = ? ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? - ; chain⊆A = ? ; f-next = ? ; f-total = ? } where + no-extension ¬sp=x = record { supf = supf1 ; supf-mono = {!!} ; 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-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 + ... | 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 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s @@ -772,8 +674,8 @@ (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 ) (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 + ... | 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 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s @@ -781,48 +683,48 @@ (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 ) (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 + ... | tri> ¬a ¬b px<s | record {eq = eq1} = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x {!!} )) where s≤u : s o≤ u - s≤u = ? + s≤u = {!!} u=x : u ≡ x u=x with trio< u x - ... | tri< a ¬b ¬c = ? + ... | tri< a ¬b ¬c = {!!} ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ? - ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 ?) )) where + ... | tri> ¬a ¬b c = {!!} + ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 {!!}) )) where u=x : u ≡ x u=x with trio< u x - ... | tri< a ¬b ¬c = ? + ... | tri< a ¬b ¬c = {!!} ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ? + ... | tri> ¬a ¬b c = {!!} sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) sup {z} z≤x with trio< z px - ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup zc (o<→≤ a)) - ... | tri≈ ¬a b ¬c = SUP⊆ ? (ZChain.sup zc (o≤-refl0 b)) - ... | tri> ¬a ¬b c = SUP⊆ ? sup1 + ... | tri< a ¬b ¬c = SUP⊆ {!!} (ZChain.sup zc (o<→≤ a)) + ... | tri≈ ¬a b ¬c = SUP⊆ {!!} (ZChain.sup zc (o≤-refl0 b)) + ... | tri> ¬a ¬b c = SUP⊆ {!!} sup1 zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) - ... | no noax = no-extension ? -- ¬ A ∋ p, just skip + ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf x - ... | case1 pr = no-extension ? -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next + ... | 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 = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = ? ; supf-is-sup = ? ; supf-mono = ? } where + ; supf-mono = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!} } 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 = ? } + supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } spx = & (SUP.sup supx ) x=spx : x ≡ spx - x=spx = ? + x=spx = {!!} psupf1 : Ordinal → Ordinal psupf1 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf zc z ... | tri≈ ¬a b ¬c = x ... | tri> ¬a ¬b c = x - ... | case2 ¬x=sup = no-extension ? -- px is not f y' nor sup of former ZChain from y -- no extention + ... | case2 ¬x=sup = no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention ... | no lim = zc5 where @@ -894,23 +796,23 @@ 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 = ? ; supf-is-sup = ? - ; csupf = ? ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; supf-mono = ? } where + ; sup = {!!} ; supf-is-sup = {!!} + ; csupf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; supf-mono = {!!} } 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 - UnionCF⊆ = ? + UnionCF⊆ = {!!} zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) - ... | no noax = no-extension ? -- ¬ A ∋ p, just skip + ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f ) -- we have to check adding x preserve is-max ZChain A y f mf x - ... | case1 pr = no-extension ? + ... | 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 = ? - ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; supf-mono = ? } 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 + ; sup = {!!} ; supf-is-sup = {!!} + ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; supf-mono = {!!} } 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) SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A)