Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/zorn.agda @ 782:e8cf9c453431

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Aug 2022 09:38:00 +0900
parents 460df9965d63
children 195c3c7de021
comparison
equal deleted inserted replaced
781:460df9965d63 782:e8cf9c453431
263 record SUP ( A B : HOD ) : Set (Level.suc n) where 263 record SUP ( A B : HOD ) : Set (Level.suc n) where
264 field 264 field
265 sup : HOD 265 sup : HOD
266 A∋maximal : A ∋ sup 266 A∋maximal : A ∋ sup
267 x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive 267 x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive
268 min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) )
269 → (z ≡ sup ) ∨ (sup < z )
268 270
269 -- 271 --
270 -- sup and its fclosure is in a chain HOD 272 -- sup and its fclosure is in a chain HOD
271 -- chain HOD is sorted by sup as Ordinal and <-ordered 273 -- chain HOD is sorted by sup as Ordinal and <-ordered
272 -- whole chain is a union of separated Chain 274 -- whole chain is a union of separated Chain
278 fcy<sup : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 280 fcy<sup : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u )
279 order : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) 281 order : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
280 282
281 -- Union of supf z which o< x 283 -- Union of supf z which o< x
282 -- 284 --
283
284 -- data DChain ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) : (z : Ordinal) → Set n where
285 -- dinit : DChain f mf ay (& (SUP.sup (ysup f mf ay)))
286 -- dsuc : {u : Ordinal } → (au : odef A u) → DChain f mf ay u → DChain f mf ay ( & (SUP.sup (ysup f mf au)) )
287 285
288 data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) 286 data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
289 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 287 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where
290 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z 288 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
291 ch-is-sup : (u : Ordinal) {z : Ordinal } ( is-sup : ChainP A f mf ay supf u z) 289 ch-is-sup : (u : Ordinal) {z : Ordinal } ( is-sup : ChainP A f mf ay supf u z)
310 chain∋init : odef chain init 308 chain∋init : odef chain init
311 initial : {y : Ordinal } → odef chain y → * init ≤ * y 309 initial : {y : Ordinal } → odef chain y → * init ≤ * y
312 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 310 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
313 f-total : IsTotalOrderSet chain 311 f-total : IsTotalOrderSet chain
314 312
313 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x)
314 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
315 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 315 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
316 csupf : (z : Ordinal ) → odef chain (supf z)
317 csupf' : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b)
316 fcy<sup : {u w : Ordinal } → u o< z → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 318 fcy<sup : {u w : Ordinal } → u o< z → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
317 order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) 319 order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
320 supf∈A : {u : Ordinal } → odef A (supf u)
321 supf∈A = ?
322 fcy<sup' : {u w : Ordinal } → u o< z → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
323 fcy<sup' {u} {w} u<z fc with SUP.x<sup (sup ?) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} init f mf fc) , ? ⟫
324 ... | case1 eq = ?
325 ... | case2 lt = ?
326 fc∈A : {s z1 : Ordinal} → FClosure A f (supf s) z1 → odef chain z1
327 fc∈A {s} (fsuc x fc) = f-next (fc∈A {s} fc ) -- (supf s) ≡ z1 → init (supf s)
328 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)
329 order' {b} {s} {z1} b<z sf<sb fc with SUP.x<sup (sup (o<→≤ b<z)) (subst (λ k → odef (UnionCF A f mf ay supf b) k) (sym &iso) ( csupf' (o<→≤ b<z)) )
330 ... | case1 eq = case1 (begin
331 ? ≡⟨ ? ⟩
332 ? ∎ ) where open ≡-Reasoning
333 ... | case2 lt = case2 ? where
334 zc00 : ?
335 zc00 = ?
336 -- case2 ( subst (λ k → * z1 < k ) (subst₂ (λ j k → j ≡ k ) *iso ? (cong (*) (sym supf-is-sup))) lt )
318 337
319 338
320 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 339 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
321 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 340 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
322 field 341 field
327 record Maximal ( A : HOD ) : Set (Level.suc n) where 346 record Maximal ( A : HOD ) : Set (Level.suc n) where
328 field 347 field
329 maximal : HOD 348 maximal : HOD
330 A∋maximal : A ∋ maximal 349 A∋maximal : A ∋ maximal
331 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative 350 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative
351
352 --
353
354 supf-unique : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
355 → {a b : Ordinal } → a o< b
356 → (za : ZChain A f mf ay (osuc a) ) → (zb : ZChain A f mf ay (osuc b) )
357 → odef (UnionCF A f mf ay (ZChain.supf za) (osuc a)) (ZChain.supf za a)
358 → odef (UnionCF A f mf ay (ZChain.supf zb) (osuc b)) (ZChain.supf zb a) → ZChain.supf za a ≡ ZChain.supf zb a
359 supf-unique A f mf {y} ay {a} {b} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-init fcb ⟫ = ? where
360 supf = ZChain.supf za
361 supb = ZChain.supf zb
362 su00 : {u w : Ordinal } → u o< osuc a → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u )
363 su00 = ZChain.fcy<sup za
364 su01 : (supf a ≡ supb b ) ∨ ( supf a << supb b )
365 su01 = ZChain.fcy<sup zb <-osuc fca
366 su02 : (supb a ≡ supf a ) ∨ ( supb a << supf a )
367 su02 = ZChain.fcy<sup za <-osuc fcb
368 supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
369 supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-init fcb ⟫ = ?
370 supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
332 371
333 -- data UChain is total 372 -- data UChain is total
334 373
335 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 374 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
336 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) 375 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
472 zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) 511 zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
473 512
474 SZ1 :( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 513 SZ1 :( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
475 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x 514 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x
476 SZ1 A f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where 515 SZ1 A f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where
477 chain-mono2 : (x : Ordinal) {a b c : Ordinal} → a o≤ b → b o≤ x → 516 chain-mono1 : (x : Ordinal) {a b c : Ordinal} →
478 odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c 517 odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
479 chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , ch-init fc ⟫ = 518 chain-mono1 x {a} {b} {c} ⟪ ua , ch-init fc ⟫ =
480 ⟪ ua , ch-init fc ⟫ 519 ⟪ ua , ch-init fc ⟫
481 chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa , ch-is-sup ua is-sup fc ⟫ = 520 chain-mono1 x {a} {b} {c} ⟪ uaa , ch-is-sup ua is-sup fc ⟫ =
482 ⟪ uaa , ch-is-sup ua is-sup fc ⟫ 521 ⟪ uaa , ch-is-sup ua is-sup fc ⟫
483 chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A) 522 chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
484 chain<ZA {x} ux with proj2 ux 523 chain<ZA {x} ux with proj2 ux
485 ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫ 524 ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫
486 ... | ch-is-sup u is-sup fc = ⟪ proj1 ux , ch-is-sup u is-sup fc ⟫ 525 ... | ch-is-sup u is-sup fc = ⟪ proj1 ux , ch-is-sup u is-sup fc ⟫
510 px<x : px o< x 549 px<x : px o< x
511 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc 550 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
512 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b 551 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
513 m01 with trio< b px --- px < b < x 552 m01 with trio< b px --- px < b < x
514 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫) 553 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫)
515 ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl m04 where 554 ... | tri< b<px ¬b ¬c = chain-mono1 x m04 where
516 m03 : odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used 555 m03 : odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
517 m03 with proj2 ua 556 m03 with proj2 ua
518 ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫ 557 ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫
519 ... | ch-is-sup u is-sup-a fc = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫ 558 ... | ch-is-sup u is-sup-a fc = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫
520 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b 559 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
521 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 560 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab
522 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b 561 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x lt) } ) a<b
523 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where 562 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where
524 b<A : b o< & A 563 b<A : b o< & A
525 b<A = z09 ab 564 b<A = z09 ab
526 m05 : b ≡ ZChain.supf zc b 565 m05 : b ≡ ZChain.supf zc b
527 m05 = sym ( ZChain.sup=u zc ab (z09 ab) 566 m05 = sym ( ZChain.sup=u zc ab (z09 ab)
528 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz ) } ) 567 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x uz ) } )
529 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b 568 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
530 m08 {z} fcz = ZChain.fcy<sup zc b<A fcz 569 m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
531 m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 570 m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b)
532 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b 571 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
533 m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz 572 m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
538 b o< x → (ab : odef A b) → 577 b o< x → (ab : odef A b) →
539 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 → 578 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 →
540 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 579 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
541 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 580 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b
542 is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay ) 581 is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
543 ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) ) 582 ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA {x} (chain-mono1 (osuc x) ua )) )
544 (subst (λ k → * a < * k ) (sym b=y) a<b ) ) 583 (subst (λ k → * a < * k ) (sym b=y) a<b ) )
545 ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where 584 ... | case2 y<b = chain-mono1 x m04 where
546 m09 : b o< & A 585 m09 : b o< & A
547 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) 586 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
548 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b 587 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
549 m07 {z} fc = ZChain.fcy<sup zc m09 fc 588 m07 {z} fc = ZChain.fcy<sup zc m09 fc
550 m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 589 m08 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b)
551 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b 590 → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
552 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc 591 m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
553 m05 : b ≡ ZChain.supf zc b 592 m05 : b ≡ ZChain.supf zc b
554 m05 = sym (ZChain.sup=u zc ab m09 593 m05 = sym (ZChain.sup=u zc ab m09
555 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} ) -- ZChain on x 594 record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x lt )} ) -- ZChain on x
556 m06 : ChainP A f mf ay (ZChain.supf zc) b b 595 m06 : ChainP A f mf ay (ZChain.supf zc) b b
557 m06 = record { fcy<sup = m07 ; order = m08 } 596 m06 = record { fcy<sup = m07 ; order = m08 }
558 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b 597 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
559 m04 = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ 598 m04 = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫
560 599
715 pcy : odef pchain y 754 pcy : odef pchain y
716 pcy = ⟪ ay , ch-init (init ay) ⟫ 755 pcy = ⟪ ay , ch-init (init ay) ⟫
717 756
718 supf0 = ZChain.supf zc 757 supf0 = ZChain.supf zc
719 758
759 csupf : (z : Ordinal) → odef (UnionCF A f mf ay supf0 x) (supf0 z)
760 csupf z with ZChain.csupf zc z
761 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
762 ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫
763
720 -- if previous chain satisfies maximality, we caan reuse it 764 -- if previous chain satisfies maximality, we caan reuse it
721 -- 765 --
722 no-extension : ZChain A f mf ay x 766 no-extension : ZChain A f mf ay x
723 no-extension = record { supf = supf0 767 no-extension = record { supf = supf0
724 ; initial = pinit ; chain∋init = pcy ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} 768 ; initial = pinit ; chain∋init = pcy ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!}
794 zc22 with trio< s x 838 zc22 with trio< s x
795 ... | tri< s<x ¬b ¬c = zc23 where 839 ... | tri< s<x ¬b ¬c = zc23 where
796 szc = pzc (osuc s) (ob<x lim s<x) 840 szc = pzc (osuc s) (ob<x lim s<x)
797 zc23 : ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s ≡ ZChain.supf (pzc (osuc b) (ob<x lim a)) s 841 zc23 : ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s ≡ ZChain.supf (pzc (osuc b) (ob<x lim a)) s
798 zc23 = ? 842 zc23 = ?
843 zc24 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc s) (ob<x lim s<x))) (osuc s))
844 (ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s )
845 zc24 = ZChain.csupf (pzc (osuc s) (ob<x lim s<x)) s
846 zc25 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim a))) (osuc b))
847 (ZChain.supf (pzc (osuc b) (ob<x lim a)) b )
848 zc25 = ZChain.csupf (pzc (osuc b) (ob<x lim a)) b
849
799 ... | tri≈ ¬a b ¬c = ? 850 ... | tri≈ ¬a b ¬c = ?
800 ... | tri> ¬a ¬b c = ? 851 ... | tri> ¬a ¬b c = ?
801 zc21 : ZChain.supf uzc s o< ZChain.supf uzc b 852 zc21 : ZChain.supf uzc s o< ZChain.supf uzc b
802 zc21 = subst (λ k → k o< _) zc22 ps<pb 853 zc21 = subst (λ k → k o< _) zc22 ps<pb
803 zc20 : FClosure A f (ZChain.supf uzc s ) z1 854 zc20 : FClosure A f (ZChain.supf uzc s ) z1
804 zc20 = subst (λ k → FClosure A f k z1) zc22 fc 855 zc20 = subst (λ k → FClosure A f k z1) zc22 fc
805 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a b<x) 856 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a b<x)
806 ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x) 857 ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x)
858
859 csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
860 csupf z with trio< z x | inspect psupf z
861 ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
862 ozc = pzc (osuc z) (ob<x lim z<x)
863 zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
864 zc12 = ZChain.csupf ozc z
865 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
866 zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) ⟫ where
867 az : odef A ( ZChain.supf ozc z )
868 az = proj1 zc12
869 zc20 : {z1 : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
870 zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
871 ... | case1 eq = case1 (trans eq (sym eq1) )
872 ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
873 cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
874 cp1 = record { fcy<sup = zc20 ; order = order z<x }
875 --- u = supf u = supf z
876 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
877 sa = SUP.A∋maximal usup
878 ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
879
807 880
808 fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u) 881 fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u)
809 fcy<sup {u} {w} u<x fc with trio< u x 882 fcy<sup {u} {w} u<x fc with trio< u x
810 ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where 883 ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where
811 uzc = pzc (osuc u) (ob<x lim a) 884 uzc = pzc (osuc u) (ob<x lim a)