Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 799:c8a166abcae0
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 07 Aug 2022 18:39:18 +0900 |
parents | 9cf74877efab |
children | 06eedb0d26a0 |
comparison
equal
deleted
inserted
replaced
798:9cf74877efab | 799:c8a166abcae0 |
---|---|
189 | 189 |
190 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 | 190 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 |
191 field | 191 field |
192 fcy<sup : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) | 192 fcy<sup : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) |
193 order : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) | 193 order : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) |
194 supu=u : o∅ o< u → supf u ≡ u | 194 supu=u : supf u ≡ u |
195 | 195 |
196 -- Union of supf z which o< x | 196 -- Union of supf z which o< x |
197 -- | 197 -- |
198 | 198 |
199 data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) | 199 data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) |
227 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 | 227 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 |
228 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) | 228 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) |
229 csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) | 229 csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) |
230 supf≤x :{x : Ordinal } → z o≤ x → supf z ≡ supf x | 230 supf≤x :{x : Ordinal } → z o≤ x → supf z ≡ supf x |
231 | 231 |
232 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 | 232 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 |
233 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) | 233 fcy<sup {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) |
234 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ | 234 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ |
235 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) )) | 235 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) )) |
236 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt ) | 236 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt ) |
237 | 237 |
238 supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y | 238 supf-mono : {x y1 : Ordinal } → x o< y1 → supf x o≤ supf y1 |
239 supf-mono {x} {y} x<y = sf<sy where | 239 supf-mono {x} {y1} x<y1 = sf<sy1 where |
240 -- supf x << supf y → supf x o< supf y | 240 -- supf x << supf y1 → supf x o< supf y1 |
241 -- x o< y → supf x <= supf y | 241 -- x o< y1 → supf x <= supf y1 |
242 -- z o≤ x → supf x ≡ supf y ≡ supf z | 242 -- z o≤ x → supf x ≡ supf y1 ≡ supf z |
243 -- x o< z → z o< y → supf x ≡ supf y ≡ supf z | 243 -- x o< z → z o< y1 → supf x ≡ supf y1 ≡ supf z |
244 sf<sy : supf x o≤ supf y | 244 supy : {x : Ordinal } → x o≤ z → FClosure A f y (supf x) → supf x ≡ y |
245 sf<sy with trio< x z | 245 supy {x} x≤z fcx = ? where |
246 ... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y ) <-osuc ) ) )) | 246 zc06 : ( * y ≡ SUP.sup (sup x≤z )) ∨ ( * y < SUP.sup ( sup x≤z ) ) |
247 ... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y) b (o<→≤ x<y)))) | 247 zc06 = SUP.x<sup (sup x≤z) ⟪ subst (λ k → odef A k ) (sym &iso) ay , ch-init (init ay (sym &iso) ) ⟫ |
248 ... | tri< x<z ¬b ¬c with trio< (supf x) (supf y) | 248 sf<sy1 : supf x o≤ supf y1 |
249 sf<sy1 with trio< x z | |
250 ... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y1 ) <-osuc ) ) )) | |
251 ... | 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)))) | |
252 ... | tri< x<z ¬b ¬c with trio< (supf x) (supf y1) | |
249 ... | tri< a ¬b ¬c = o<→≤ a | 253 ... | tri< a ¬b ¬c = o<→≤ a |
250 ... | tri≈ ¬a b ¬c = o≤-refl0 b | 254 ... | tri≈ ¬a b ¬c = o≤-refl0 b |
251 ... | tri> ¬a ¬b sy<sx with trio< z y | 255 ... | tri> ¬a ¬b sy1<sx with trio< z y1 |
252 ... | tri< a ¬b ¬c = ? | 256 ... | tri< a ¬b ¬c = ? |
253 ... | tri≈ ¬a b ¬c = ? | 257 ... | tri≈ ¬a b ¬c = ? |
254 ... | tri> ¬a ¬b y<z = ? | 258 ... | tri> ¬a ¬b y1<z = ? |
255 zc04 : x o< z → y o< z → supf x o≤ supf y | 259 zc04 : x o< z → y1 o≤ z → supf x o≤ supf y1 |
256 zc04 x<z y<z with csupf (o<→≤ x<z) | csupf (o<→≤ y<z) | 260 zc04 x<z y1≤z with csupf (o<→≤ x<z) | csupf y1≤z |
257 ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy | 261 ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ with fcy<sup (o<→≤ x<z) fcy1 |
258 ... | case1 eq = o≤-refl0 (sym eq) | 262 ... | case1 eq = o≤-refl0 (sym eq) |
259 ... | case2 lt with fcy<sup y<z fcx | 263 ... | case2 lt with fcy<sup y1≤z fcx |
260 ... | case1 eq = o≤-refl0 eq | 264 ... | case1 eq = o≤-refl0 eq |
261 ... | case2 lt1 = ⊥-elim ( <-irr (case2 lt) lt1 ) | 265 ... | case2 lt1 = ⊥-elim ( <-irr (case2 lt) lt1 ) |
262 zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy | 266 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 |
263 ... | case1 eq = o≤-refl0 (sym eq) | 267 ... | case1 eq = o≤-refl0 (sym eq) |
264 ... | case2 lt with ChainP.fcy<sup is-sup-x fcy | 268 ... | case2 lt with trio< (supf x) (supf y1) |
265 ... | case1 eq with s≤fc (supf ux) f mf fcx | 269 ... | tri< a ¬b ¬c = o<→≤ a |
266 ... | case1 eq1 = o≤-refl0 ( trans ( subst₂ (λ j k → j ≡ k ) &iso &iso (sym (cong (&) eq1))) (sym eq) ) | 270 ... | tri≈ ¬a b ¬c = o≤-refl0 b |
267 ... | case2 lt1 = ? -- ux << sx, sy << sx | 271 ... | tri> ¬a ¬b y1<z = ? where |
268 zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ | case2 lt1 = ? -- sy << sx | 272 zc05 : ( supf y1 ≡ supf ux ) ∨ (supf y1 << supf ux ) |
269 zc04 x<z y<z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ? | 273 zc05 = ChainP.fcy<sup is-sup-x fcy1 |
270 zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ? | 274 zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ | case2 lt1 = ? -- sy1 << sx |
275 zc04 x<z y1≤z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-is-sup uy1 uy1≤z is-sup-y1 fcy1 ⟫ = ? | |
276 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 ⟫ = ? | |
271 -- ... | tri< a ¬b ¬c = csupf (o<→≤ a) | 277 -- ... | tri< a ¬b ¬c = csupf (o<→≤ a) |
272 -- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b) | 278 -- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b) |
273 -- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay supf x) k ) ? (csupf ? ) | 279 -- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay1 supf x) k ) ? (csupf ? ) |
274 -- csy : odef (UnionCF A f mf ay supf y) (supf y) | 280 -- csy1 : odef (UnionCF A f mf ay1 supf y1) (supf y1) |
275 -- csy = csupf ? | 281 -- csy1 = csupf ? |
276 | 282 |
277 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) | 283 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) |
278 order {b} {s} {z1} b<z sf<sb fc = zc04 where | 284 order {b} {s} {z1} b<z sf<sb fc = zc04 where |
279 zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 | 285 zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 |
280 zc01 (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03 where | 286 zc01 (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03 where |
494 b<A = z09 ab | 500 b<A = z09 ab |
495 m05 : b ≡ ZChain.supf zc b | 501 m05 : b ≡ ZChain.supf zc b |
496 m05 = sym ( ZChain.sup=u zc ab (z09 ab) | 502 m05 = sym ( ZChain.sup=u zc ab (z09 ab) |
497 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz ) } ) | 503 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz ) } ) |
498 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b | 504 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b |
499 m08 {z} fcz = ZChain.fcy<sup zc b<A fcz | 505 m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz |
500 m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) | 506 m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) |
501 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b | 507 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b |
502 m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz | 508 m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz |
503 m06 : ChainP A f mf ay (ZChain.supf zc) b | 509 m06 : ChainP A f mf ay (ZChain.supf zc) b |
504 m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = λ _ → ZChain.sup=u zc ab b<A {!!} } | 510 m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = ZChain.sup=u zc ab b<A {!!} } |
505 ... | no lim = record { is-max = is-max } where | 511 ... | no lim = record { is-max = is-max } where |
506 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → | 512 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → |
507 b o< x → (ab : odef A b) → | 513 b o< x → (ab : odef A b) → |
508 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → | 514 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → |
509 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b | 515 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b |
513 ... | case2 y<b = chain-mono1 (osucc b<x) | 519 ... | case2 y<b = chain-mono1 (osucc b<x) |
514 ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc ) m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫ where | 520 ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc ) m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫ where |
515 m09 : b o< & A | 521 m09 : b o< & A |
516 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) | 522 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) |
517 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b | 523 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b |
518 m07 {z} fc = ZChain.fcy<sup zc m09 fc | 524 m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc |
519 m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) | 525 m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) |
520 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b | 526 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b |
521 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc | 527 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc |
522 m05 : b ≡ ZChain.supf zc b | 528 m05 : b ≡ ZChain.supf zc b |
523 m05 = sym (ZChain.sup=u zc ab m09 | 529 m05 = sym (ZChain.sup=u zc ab m09 |
524 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} ) -- ZChain on x | 530 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} ) -- ZChain on x |
525 m06 : ChainP A f mf ay (ZChain.supf zc) b | 531 m06 : ChainP A f mf ay (ZChain.supf zc) b |
526 m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = λ _ → ZChain.sup=u zc ab m09 {!!} } | 532 m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = ZChain.sup=u zc ab m09 {!!} } |
527 | 533 |
528 --- | 534 --- |
529 --- the maximum chain has fix point of any ≤-monotonic function | 535 --- the maximum chain has fix point of any ≤-monotonic function |
530 --- | 536 --- |
531 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) | 537 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) |
640 spi ∎ ) where open ≡-Reasoning | 646 spi ∎ ) where open ≡-Reasoning |
641 ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt ) | 647 ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt ) |
642 uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi) | 648 uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi) |
643 uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi ) | 649 uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi ) |
644 uz02 : ChainP A f mf ay isupf o∅ | 650 uz02 : ChainP A f mf ay isupf o∅ |
645 uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = λ lt → ⊥-elim ( o<¬≡ refl lt ) } | 651 uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = ? } |
646 | 652 |
647 SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B | 653 SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B |
648 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) } | 654 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) } |
649 | 655 |
650 -- | 656 -- |
730 u=x : u ≡ x | 736 u=x : u ≡ x |
731 u=x with trio< u x | 737 u=x with trio< u x |
732 ... | tri< a ¬b ¬c = {!!} | 738 ... | tri< a ¬b ¬c = {!!} |
733 ... | tri≈ ¬a b ¬c = b | 739 ... | tri≈ ¬a b ¬c = b |
734 ... | tri> ¬a ¬b c = {!!} | 740 ... | tri> ¬a ¬b c = {!!} |
735 ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 {!!}) )) where | 741 ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x su=u1 )) where |
736 u=x : u ≡ x | 742 u=x : u ≡ x |
737 u=x with trio< u x | 743 u=x with trio< u x |
738 ... | tri< a ¬b ¬c = {!!} | 744 ... | tri< a ¬b ¬c = {!!} |
739 ... | tri≈ ¬a b ¬c = b | 745 ... | tri≈ ¬a b ¬c = b |
740 ... | tri> ¬a ¬b c = {!!} | 746 ... | tri> ¬a ¬b c = {!!} |
794 supf1 : Ordinal → Ordinal | 800 supf1 : Ordinal → Ordinal |
795 supf1 z with trio< z x | 801 supf1 z with trio< z x |
796 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z | 802 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z |
797 ... | tri≈ ¬a b ¬c = spu | 803 ... | tri≈ ¬a b ¬c = spu |
798 ... | tri> ¬a ¬b c = spu | 804 ... | tri> ¬a ¬b c = spu |
799 | |
800 fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ supf1 u) ∨ (w << supf1 u) | |
801 fcy<sup {u} {w} u<x fc with trio< u x | |
802 ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where | |
803 uzc = pzc (osuc u) (ob<x lim a) | |
804 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a u<x) | |
805 ... | tri> ¬a ¬b c = ⊥-elim (¬a u<x) | |
806 | 805 |
807 pchain : HOD | 806 pchain : HOD |
808 pchain = UnionCF A f mf ay supf1 x | 807 pchain = UnionCF A f mf ay supf1 x |
809 | 808 |
810 pchain⊆A : {y : Ordinal} → odef pchain y → odef A y | 809 pchain⊆A : {y : Ordinal} → odef pchain y → odef A y |