Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 890:3eaf3b8b1009
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 04 Oct 2022 10:46:22 +0900 |
| parents | 450225f4d55d |
| children | 9fb948dac666 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 70 insertions(+), 62 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 03 19:00:35 2022 +0900 +++ b/src/zorn.agda Tue Oct 04 10:46:22 2022 +0900 @@ -350,7 +350,7 @@ UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD UnionCF A f mf ay supf x - = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } + = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf (supf x) z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) → supf x o< supf y → x o< y @@ -395,7 +395,7 @@ asupf : {x : Ordinal } → odef A (supf x) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y - x≤supfx : {x : Ordinal } → x o≤ z → x o≤ supf x + x≤supfx : {x : Ordinal } → x o≤ supf z → x o≤ supf x minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (M→S supf (minsup x≤z) )) @@ -459,7 +459,7 @@ {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where supf = ZChain.supf zc field - is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z → (ab : odef A b) + is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< supf z → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf z) b f ∨ IsSup A (UnionCF A f mf ay supf z) ab → * a < * b → odef ((UnionCF A f mf ay supf z)) b @@ -572,7 +572,7 @@ cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ chain-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) - {a b c : Ordinal} → a o≤ b + {a b c : Ordinal} → supf a o≤ supf b → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ @@ -595,17 +595,17 @@ SZ1 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x SZ1 f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where - chain-mono1 : {a b c : Ordinal} → a o≤ b + chain-mono1 : {a b c : Ordinal} → (ZChain.supf zc a) o≤ (ZChain.supf zc b) → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → - b o< x → (ab : odef A b) → + b o< ZChain.supf zc x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , - subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) + subst (λ k → UChain A f mf ay (ZChain.supf zc) (ZChain.supf zc x) k ) (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ supf = ZChain.supf zc @@ -621,7 +621,7 @@ zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 zc08) is-sup fc ⟫ where + ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc10 is-sup fc ⟫ where zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s zc07 = fc zc06 : supf u ≡ u @@ -632,6 +632,8 @@ zc09 u≤s with osuc-≡< u≤s ... | case1 u=ss = ZChain.supf-inject zc (subst (λ k → k o< supf b) (sym (trans zc06 u=ss)) ss<sb ) ... | case2 u<ss = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<ss)) s<b + zc10 : u o< supf b + zc10 = ordtrans≤-< zc08 ss<sb 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 (csupf-fc b<z ss≤sb fc ) @@ -654,7 +656,7 @@ zc-b<x : {b : Ordinal } → b o< x → b o< osuc px zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → - b o< x → (ab : odef A b) → + b o< ZChain.supf zc x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → * a < * b → odef (UnionCF A f mf ay supf x) b is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P @@ -664,11 +666,11 @@ b<A : b o< & A b<A = z09 ab m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f - m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) + m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 ? (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) - ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz ) } , m04 ⟫ + ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? uz ) } , m04 ⟫ 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 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -678,15 +680,15 @@ m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 } ... | no lim = record { is-max = is-max } where is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → - b o< x → (ab : odef A b) → + b o< ZChain.supf zc x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → * a < * b → odef (UnionCF A f mf ay supf x) b is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ - ... | case2 y<b = chain-mono1 (osucc b<x) - ⟪ ab , ch-is-sup b <-osuc m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where + ... | case2 y<b = chain-mono1 ? + ⟪ ab , ch-is-sup b ? m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where m09 : b o< & A 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 @@ -695,11 +697,11 @@ → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b m08 {s} {z1} s<b fc = order m09 s<b fc m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f - m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) + m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 ? (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b m05 = ZChain.sup=u zc ab (o<→≤ m09) - ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫ -- ZChain on x + ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 ? lt )} , m04 ⟫ -- ZChain on x m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } @@ -711,12 +713,12 @@ fixpoint f mf zc = z14 where chain = ZChain.chain zc sp1 = sp0 f mf as0 zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< ZChain.supf zc (& A) → (ab : odef A b ) → HasPrev A chain b f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) - z11 : & (SUP.sup sp1) o< & A - z11 = c<→o< ( SUP.as sp1) + z11 : & (SUP.sup sp1) o< ZChain.supf zc (& A) + z11 = ? -- c<→o< ( SUP.as sp1) z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) @@ -813,10 +815,13 @@ pchain : HOD pchain = UnionCF A f mf ay supf0 px - -- ¬ supf0 px ≡ px → UnionCF supf0 px ≡ UnionCF supf1 x + -- px o< supf0 px → UnionCF supf0 px ≡ UnionCF supf1 x -- supf1 x ≡ supf0 px - -- supf0 px ≡ px → ( UnionCF A f mf ay supf0 px ∪ FClosure px ) ≡ UnionCF supf1 x - -- supf1 x ≡ sup of ( UnionCF A f mf ay supf0 px ∪ FClosure px (= UnionCF supf1 x))) ≥ supf0 px + -- px ≡ supf0 px → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x + -- supf1 x ≡ sup of ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) (= UnionCF supf1 x))) -- nsup ≥ supf0 px + -- supf0 px o< px → ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x + -- nsup o≥ supf0 px → supf1 x ≡ nsup + -- nsup o< supf0 px → ? supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b supf-mono = ZChain.supf-mono zc @@ -830,7 +835,7 @@ ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) zc4 : ZChain A f mf ay x - zc4 with osuc-≡< (ZChain.x≤supfx zc o≤-refl ) + zc4 with osuc-≡< (ZChain.x≤supfx zc ? ) ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1 ; x≤supfx = ? ; minsup = ? ; supf-is-sup = ? ; csupf = ? } where @@ -839,15 +844,15 @@ -- supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and FClosure px pchainpx : HOD - pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z } ; odmax = & A ; <odmax = zc00 } where - zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A + pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 (supf0 px) z ) ∨ FClosure A f px z } ; odmax = & A ; <odmax = zc00 } where + zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 (supf0 px) z ) ∨ FClosure A f px z → z o< & A zc00 {z} (case1 lt) = z07 lt zc00 {z} (case2 fc) = z09 ( A∋fc px f mf fc ) - zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → odef A z + zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 (supf0 px) z ) ∨ FClosure A f px z → odef A z zc01 {z} (case1 lt) = proj1 lt zc01 {z} (case2 fc) = ( A∋fc px f mf fc ) - zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b + zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 (supf0 px) a → FClosure A f px b → a <= b zc02 {a} {b} ca fb = zc05 fb where zc06 : & (SUP.sup (ZChain.sup zc o≤-refl)) ≡ px zc06 = trans (sym ( ZChain.supf-is-sup zc o≤-refl )) (sym sfpx=px) @@ -856,7 +861,7 @@ ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) zc05 (init b1 refl) with SUP.x<sup (ZChain.sup zc o≤-refl) - (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca ) + ? -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 ? k) (sym &iso) ca ) ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 (cong (&) eq)) ... | case2 lt = case2 (subst (λ k → (* a) < k ) (trans (sym *iso) (cong (*) zc06)) lt) @@ -920,9 +925,9 @@ supf-mono1 {z} {w} z≤w | tri> ¬a ¬b c with trio< z px ... | tri< a ¬b ¬c = zc19 where zc21 : MinSUP A (UnionCF A f mf ay supf0 z) - zc21 = ZChain.minsup zc (o<→≤ a) + zc21 = ZChain.minsup zc ? -- (o<→≤ a) zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) - zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a) ux)) + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux)) zc19 : supf0 z o≤ sp1 zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc (o<→≤ a))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri≈ ¬a b ¬c = zc18 where @@ -935,7 +940,7 @@ supf0 px ≡⟨ sym sfpx=px ⟩ px ∎ where open ≡-Reasoning zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 z) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1) - zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o≤-refl0 b) ux)) + zc24 {x₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 ? ux)) zc18 : px o≤ sp1 -- supf0 z ≡ px zc18 = subst (λ k → k o≤ sp1) zc20 ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri> ¬a ¬b c = o≤-refl @@ -993,20 +998,20 @@ ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ ... | case2 fc = case2 (fsuc _ fc) zc21 (init asp refl ) with trio< u px | inspect supf1 u - ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17 + ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where zc19 : u o≤ px - zc19 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x + zc19 = subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? -- u<x zc18 : s o≤ px zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) ... | tri≈ ¬a b ¬c | _ = case2 (init apx refl ) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) ? ⟫ ) zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where @@ -1016,19 +1021,19 @@ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with trio< u px | inspect supf1 u ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u - (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc )) - record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans ((sf1=sf0 (o<→≤ u<x))) (ChainP.supu=u is-sup) } zc14 ⟫ where + ? -- (subst (λ k → u o< k) (Oprev.oprev=x op) ?) + record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans ((sf1=sf0 ?)) (ChainP.supu=u is-sup) } zc14 ⟫ where zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.order is-sup - (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<x)) ss<spx) (fcup fc s≤px) ) where + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 ?)) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ?) ss<spx) (fcup fc s≤px) ) where s≤px : s o≤ px - s≤px = ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u<x) + s≤px = ? -- ordtrans ( supf-inject0 supf-mono1 ss<spx ) (o<→≤ u<x) zc14 : FClosure A f (supf1 u) (supf0 u) - zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 (o<→≤ u<x))) asp) (sf1=sf0 (o<→≤ u<x)) + zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?) zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc ) - ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (pxo<x op) record { fcy<sup = zc13 + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ?)) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) @@ -1047,13 +1052,13 @@ zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) s≤px : s o≤ px s≤px = o<→≤ (supf-inject0 supf-mono1 ss<spx) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , (ordtrans u<x <-osuc ) ⟫ ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ? ⟫ ) zc12 {z} (case2 fc) = zc21 fc where zc21 : {z1 : Ordinal } → FClosure A f px z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ - zc21 (init asp refl ) = ⟪ asp , ch-is-sup px (pxo<x op) + zc21 (init asp refl ) = ⟪ asp , ch-is-sup px ? record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where zc15 : supf1 px ≡ px zc15 = trans (sf1=sf0 o≤-refl ) (sym sfpx=px) @@ -1076,21 +1081,21 @@ -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 csupf17 (init as refl ) = ZChain.csupf zc sf<px - csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) + csupf17 (fsuc x fc) = ? -- ZChain.f-next zc ? -- (csupf17 fc) - x≤supfx1 : {z : Ordinal} → z o≤ x → z o≤ supf1 z + x≤supfx1 : {z : Ordinal} → z o≤ supf1 x → z o≤ supf1 z x≤supfx1 {z} z≤x with trio< z (supf1 z) -- supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px ... | tri< a ¬b ¬c = o<→≤ a ... | tri≈ ¬a b ¬c = o≤-refl0 b ... | tri> ¬a ¬b c with trio< z px - ... | tri< a ¬b ¬c = ZChain.x≤supfx zc (o<→≤ a) + ... | tri< a ¬b ¬c = ZChain.x≤supfx zc ? ... | tri≈ ¬a b ¬c = subst (λ k → k o< osuc px) (sym b) <-osuc ... | tri> ¬a ¬b lt = ⊥-elim ( o≤> sf04 c ) where -- c : sp1 o< z, lt : px o< z -- supf1 z ≡ sp1 -- supf1 z o< z z=x : z ≡ x z=x with trio< z x ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ lt , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x c ) + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤x ? ) sf01 : supf1 x ≡ sp1 sf01 with trio< x px ... | tri< a ¬b ¬c = ⊥-elim ( ¬c (pxo<x op )) @@ -1102,7 +1107,10 @@ sf00 = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) sf01 sf02 sf04 : z o≤ sp1 sf04 with osuc-≡< sf00 - ... | case1 eq = ? where -- sup of U px ≡ supf1 px ≡ supf1 x ≡ sp1 ≡ sup of U x + ... | case1 eq = ? -- sup of U px ≡ supf1 px ≡ supf1 x ≡ sp1 ≡ sup of U x + -- px ≡ supf0 px + -- px ≡ supf1 x + -- supf1 x ≡ x ? ... | case2 lt = subst (λ k → k o≤ sp1 ) (trans (Oprev.oprev=x op) (sym z=x)) (osucc lt ) record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where @@ -1128,7 +1136,7 @@ z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a )) ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where z1≤px : z1 o≤ px -- z1 o≤ supf1 z1 ≡ px - z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) )) + z1≤px = subst (λ k → z1 o< k) (sym (Oprev.oprev=x op)) (supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 ? ) )) zc20 : supf0 px ≡ supf1 z1 zc20 = begin supf0 px ≡⟨ sym sfpx=px ⟩ @@ -1139,7 +1147,7 @@ zc21 : px o< z1 zc21 = ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c ) zc22 : z1 o< x -- c : px o< supf0 z1 - zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 o≤-refl ) ) + zc22 = supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x (x≤supfx1 ? ) ) -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x ... | case2 px<spfx = ? where @@ -1181,7 +1189,7 @@ 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 (pxo<x op)) ? ? ⟫ + zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ? ? ⟫ zc111 : {z : Ordinal} → z o< px → OD.def (od pchain1) z → OD.def (od pchain) z zc111 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ @@ -1191,7 +1199,7 @@ → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z ) zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px - ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px ? fc ⟫ + ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 ? ? fc ⟫ ... | tri≈ ¬a eq ¬c = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 ? ⟫ where s1u=u : supf0 u1 ≡ u1 s1u=u = ? -- ChainP.supu=u u1-is-sup @@ -1202,15 +1210,15 @@ eq with trio< u1 x ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c ) + ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? ) s1u=x : supf0 u1 ≡ x s1u=x = trans ? eq zc13 : osuc px o< osuc u1 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? - x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) zc13 )) - ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 (o<→≤ u<x) ) where + x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) ? )) + ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 ? ) where zc14 : u ≡ osuc px zc14 = begin u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ @@ -1229,7 +1237,7 @@ eq with trio< u1 x ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c ) + ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? ) zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z zc20 {z} (init asu su=z ) = zc13 where zc14 : x ≡ z @@ -1331,9 +1339,9 @@ * a < * b → odef (UnionCF A f mf ay supf x) b is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , - subst (λ k → UChain A f mf ay supf x k ) - (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ + ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ? -- ⟪ ab , + -- subst (λ k → UChain A f mf ay supf x k ) + -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ zc70 : HasPrev A pchain x f → ¬ xSUP pchain x zc70 pr xsup = ? @@ -1352,7 +1360,7 @@ zc12 (fsuc x fc) with zc12 fc ... | ⟪ 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₁) ⟫ - zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u u≤x ? (init ? ? ) ⟫ + zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫ 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 u u<x is-sup fc ⟫ = zc13 fc where @@ -1361,7 +1369,7 @@ ... | ⟪ 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₁) ⟫ zc13 (init asu su=z ) with trio< u x - ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u u<x ? (init ? ? ) ⟫ + ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫ ... | tri≈ ¬a b ¬c = ? ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c ) sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)