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

comparison src/zorn.agda @ 728:e864471a818f

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, 18 Jul 2022 21:50:17 +0900
parents 322dd6569072
children ac6b4d200f27
comparison
equal deleted inserted replaced
727:322dd6569072 728:e864471a818f
293 field 293 field
294 supf : Ordinal → Ordinal 294 supf : Ordinal → Ordinal
295 chain : HOD 295 chain : HOD
296 chain = UnionCF A f mf ay supf z 296 chain = UnionCF A f mf ay supf z
297 field 297 field
298 chain-mono : {z1 : Ordinal} → z1 o≤ z → UnionCF A f mf ay supf z1 ⊆' UnionCF A f mf ay supf z
298 chain⊆A : chain ⊆' A 299 chain⊆A : chain ⊆' A
299 chain∋init : odef chain init 300 chain∋init : odef chain init
300 initial : {y : Ordinal } → odef chain y → * init ≤ * y 301 initial : {y : Ordinal } → odef chain y → * init ≤ * y
301 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 302 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
302 f-total : IsTotalOrderSet chain 303 f-total : IsTotalOrderSet chain
304
305 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
306 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
307 field
308 b<x→chain : { b : Ordinal } → b o< z → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → odef (UnionCF A f mf ay (ZChain.supf zc) z) b
309 chain-mono2 : { a b c : Ordinal } →
310 a o≤ b → b o≤ z → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
311 is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) → b o< z → (ab : odef A b)
312 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab
313 → * a < * b → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
303 314
304 record Maximal ( A : HOD ) : Set (Level.suc n) where 315 record Maximal ( A : HOD ) : Set (Level.suc n) where
305 field 316 field
306 maximal : HOD 317 maximal : HOD
307 A∋maximal : A ∋ maximal 318 A∋maximal : A ∋ maximal
345 ... | case1 eq = subst (λ k → * b < k ) eq ct05 356 ... | case1 eq = subst (λ k → * b < k ) eq ct05
346 ... | case2 lt = IsStrictPartialOrder.trans POO ct05 lt 357 ... | case2 lt = IsStrictPartialOrder.trans POO ct05 lt
347 358
348 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 359 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
349 → {x z : Ordinal } → ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z ) 360 → {x z : Ordinal } → ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
350 ChainP-next A f mf {y} ay supf {x} {z} cp = ? --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp ; au = ChainP.au cp 361 ChainP-next A f mf {y} ay supf {x} {z} cp = {!!} --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp ; au = ChainP.au cp
351 -- ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp } 362 -- ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
352 363
353 Zorn-lemma : { A : HOD } 364 Zorn-lemma : { A : HOD }
354 → o∅ o< & A 365 → o∅ o< & A
355 → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition 366 → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition
408 (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) 419 (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc)
409 sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total 420 sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total
410 zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P 421 zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
411 zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) 422 zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
412 423
413 ZChain-is-max :( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 424 SZ1 :( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
414 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) → 425 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x
415 {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) a ) → b o< & A → (ab : odef A b) 426 SZ1 A f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where
416 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab 427 zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
417 → * a < * b → odef ((UnionCF A f mf ay (ZChain.supf zc) (& A))) b 428 zc1 x prev = {!!} where
418 ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case1 has-prev) a<b = 429 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
419 subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) k ) (sym (HasPrev.x=fy has-prev)) ( ZChain.f-next zc (HasPrev.ay has-prev) ) 430 b o< x → (ab : odef A b) →
420 ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case2 is-sup) a<b = ? 431 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 →
432 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
433 is-max {a} {b} ua b<x ab (case1 has-prev) a<b = {!!}
434 is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ab f )
435 ... | case1 has-prev = m03 (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) k ) {!!} m02 ) {!!} where
436 m03 : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → b o< x → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
437 m03 = {!!}
438 m02 : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) (f (HasPrev.y has-prev))
439 m02 = ZChain.f-next zc (HasPrev.ay has-prev)
440 ... | case2 ¬fy<x with Oprev-p x
441 ... | yes op = {!!} where
442 px = Oprev.oprev op
443 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
444 m01 with trio< px b
445 ... | tri< a ¬b ¬c = ZChain1.chain-mono2 (prev px ?) ? ? m04 where
446 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
447 m04 = ZChain1.is-max (prev px ?) {!!} {!!} ab {!!} a<b
448 ... | tri≈ ¬a b ¬c = {!!}
449 ... | tri> ¬a ¬b c = {!!}
450 ... | no lim = ZChain1.chain-mono2 (prev b b<x ) ? {!!} m04 where
451 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
452 m04 = ZChain1.is-max (prev (osuc b) ? ) {!!} {!!} ab {!!} a<b
421 453
422 --- 454 ---
423 --- the maximum chain has fix point of any ≤-monotonic function 455 --- the maximum chain has fix point of any ≤-monotonic function
424 --- 456 ---
425 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) 457 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) )
429 chain = ZChain.chain zc 461 chain = ZChain.chain zc
430 sp1 = sp0 f mf zc total 462 sp1 = sp0 f mf zc total
431 z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 463 z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b )
432 → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) 464 → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
433 → * a < * b → odef chain b 465 → * a < * b → odef chain b
434 z10 = ZChain-is-max A f mf as0 zc 466 z10 = ZChain1.is-max (SZ1 A f mf as0 zc (& A) )
435 z11 : & (SUP.sup sp1) o< & A 467 z11 : & (SUP.sup sp1) o< & A
436 z11 = c<→o< ( SUP.A∋maximal sp1) 468 z11 = c<→o< ( SUP.A∋maximal sp1)
437 z12 : odef chain (& (SUP.sup sp1)) 469 z12 : odef chain (& (SUP.sup sp1))
438 z12 with o≡? (& s) (& (SUP.sup sp1)) 470 z12 with o≡? (& s) (& (SUP.sup sp1))
439 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) 471 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
482 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total 514 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
483 c = & (SUP.sup sp1) 515 c = & (SUP.sup sp1)
484 516
485 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ 517 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
486 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy 518 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
487 ; initial = isy ; f-next = inext ; f-total = itotal ; is-max = imax } where 519 ; initial = isy ; f-next = inext ; f-total = itotal ; chain-mono = {!!} } where
488 isupf : Ordinal → Ordinal 520 isupf : Ordinal → Ordinal
489 isupf z = y 521 isupf z = y
490 cy : odef (UnionCF A f mf ay isupf o∅) y 522 cy : odef (UnionCF A f mf ay isupf o∅) y
491 cy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫ 523 cy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫
492 isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z 524 isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
505 b o< o∅ → (ab : odef A b) → 537 b o< o∅ → (ab : odef A b) →
506 HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab → 538 HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
507 * a < * b → odef (UnionCF A f mf ay isupf o∅) b 539 * a < * b → odef (UnionCF A f mf ay isupf o∅) b
508 imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) ) 540 imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
509 imax {a} {b} ua b<x ab (case2 sup) a<b = ⊥-elim ( ¬x<0 b<x ) 541 imax {a} {b} ua b<x ab (case2 sup) a<b = ⊥-elim ( ¬x<0 b<x )
510
511 -- exor-sup : (B : HOD)
512 -- → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) →
513 -- → {x : Ordinal } (xa : odef A x) → HasPrev A B xa → IsSup A B xa → ⊥
514 -- exor-sup B f mf {y} ay {x} xa hasp is-sup with trio<
515 542
516 -- 543 --
517 -- create all ZChains under o< x 544 -- create all ZChains under o< x
518 -- 545 --
519 546
558 pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫ 585 pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫
559 586
560 -- if previous chain satisfies maximality, we caan reuse it 587 -- if previous chain satisfies maximality, we caan reuse it
561 -- 588 --
562 no-extension : ZChain A f mf ay x 589 no-extension : ZChain A f mf ay x
563 no-extension = record { initial = pinit ; chain∋init = pcy 590 no-extension = record { supf = {!!} ; initial = pinit ; chain∋init = pcy
564 ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } 591 ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal }
565 592
566 chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain 593 chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
567 chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = zc11 ; uchain = UChain.uchain (proj2 za) } ⟫ where 594 chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = zc11 ; uchain = UChain.uchain (proj2 za) } ⟫ where
568 zc11 : (UChain.u (proj2 za) o< x) ∨ (UChain.u (proj2 za) ≡ o∅) 595 zc11 : (UChain.u (proj2 za) o< x) ∨ (UChain.u (proj2 za) ≡ o∅)
592 ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f ) 619 ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f )
593 -- we have to check adding x preserve is-max ZChain A y f mf x 620 -- we have to check adding x preserve is-max ZChain A y f mf x
594 ... | case1 pr = no-extension -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next 621 ... | case1 pr = no-extension -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
595 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx ) 622 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
596 ... | case1 is-sup = -- x is a sup of zc 623 ... | case1 is-sup = -- x is a sup of zc
597 record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal 624 record { supf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
598 ; initial = pinit ; chain∋init = pcy } 625 ; initial = pinit ; chain∋init = pcy }
599 ... | case2 ¬x=sup = no-extension -- px is not f y' nor sup of former ZChain from y -- no extention 626 ... | case2 ¬x=sup = no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
600 ... | no op = zc5 where 627 ... | no lim = zc5 where
601 628
602 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z 629 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
603 pzc z z<x = prev z z<x 630 pzc z z<x = prev z z<x
604 631
605 psupf0 : (z : Ordinal) → Ordinal 632 psupf0 : (z : Ordinal) → Ordinal
641 zc7 = ChainP.fcy<sup is-sup (init ay) 668 zc7 = ChainP.fcy<sup is-sup (init ay)
642 pcy : odef pchain y 669 pcy : odef pchain y
643 pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫ 670 pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫
644 671
645 no-extension : ZChain A f mf ay x 672 no-extension : ZChain A f mf ay x
646 no-extension = record { initial = pinit ; chain∋init = pcy 673 no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf0 ; chain-mono = ?
647 ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } 674 ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal }
648 675
649 usup : SUP A pchain 676 usup : SUP A pchain
650 usup = supP pchain (λ lt → proj1 lt) ptotal 677 usup = supP pchain (λ lt → proj1 lt) ptotal
651 spu = & (SUP.sup usup) 678 spu = & (SUP.sup usup)
653 psupf z with trio< z x 680 psupf z with trio< z x
654 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z 681 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
655 ... | tri≈ ¬a b ¬c = spu 682 ... | tri≈ ¬a b ¬c = spu
656 ... | tri> ¬a ¬b c = spu 683 ... | tri> ¬a ¬b c = spu
657 684
658 uzc : {a : Ordinal } → (za : odef pchain a) → ZChain A f mf ay (UChain.u (proj2 za))
659 uzc {a} za with UChain.u<x (proj2 za)
660 ... | case1 u<x = pzc _ u<x
661 ... | case2 u=0 = subst (λ k → ZChain A f mf ay k ) (sym u=0) (inititalChain f mf {y} ay )
662 685
663 chain-mono : pchain ⊆' UnionCF A f mf ay psupf x 686 chain-mono : pchain ⊆' UnionCF A f mf ay psupf x
664 chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ = 687 chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ =
665 ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ 688 ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫
666 chain-mono {.(psupf0 u)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (init x) } ⟫ = 689 chain-mono {.(psupf0 u)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (init x) } ⟫ =
667 ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup ? ? } ⟫ 690 ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} {!!} } ⟫
668 chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ = 691 chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ =
669 ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup ? (fsuc x ?) } ⟫ 692 ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} (fsuc x {!!}) } ⟫
670 693
671 chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 694 chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain
672 → UnionCF A f mf ay psupf x ≡ pchain 695 → UnionCF A f mf ay psupf x ≡ pchain
673 chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono } 696 chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
674 697
676 → {p0 p1 : Ordinal → Ordinal} 699 → {p0 p1 : Ordinal → Ordinal}
677 → p0 u ≡ p1 u 700 → p0 u ≡ p1 u
678 → FClosure A f (p0 u) b → FClosure A f (p1 u) b 701 → FClosure A f (p0 u) b → FClosure A f (p1 u) b
679 fc-conv {.(p0 u)} {u} {p0} {p1} p0u=p1u (init ap0u) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) ( init (subst (λ k → odef A k) p0u=p1u ap0u )) 702 fc-conv {.(p0 u)} {u} {p0} {p1} p0u=p1u (init ap0u) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) ( init (subst (λ k → odef A k) p0u=p1u ap0u ))
680 fc-conv {_} {u} {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv {_} {u} {p0} {p1} p0u=p1u fc) 703 fc-conv {_} {u} {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv {_} {u} {p0} {p1} p0u=p1u fc)
681
682 uzc-mono : {b : Ordinal } → {ob<x : osuc b o< x }
683 → odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b → odef pchain b
684 uzc-mono {b} {ob<x} ⟪ ab , record { u = x=0 ; u<x = u<x ; uchain = ch-init .b fc } ⟫ =
685 ⟪ ab , record { u = x=0 ; u<x = case2 refl ; uchain = ch-init b fc } ⟫
686 uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case2 x=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ?
687 uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ =
688 ⟪ ab , record { u = u ; u<x = case1 (ordtrans u<x ob<x) ; uchain = ch-is-sup uzc00
689 (fc-conv {b} {u} {ZChain.supf (prev (osuc b) ob<x)} {psupf0} uzc01 fc) } ⟫ where
690 uzc01 : ZChain.supf (prev (osuc b) ob<x) u ≡ psupf0 u
691 uzc01 = ? -- trans (sym (psupf0=pzc (ordtrans u<x ob<x ) )) ?
692 uzc00 : ChainP A f mf ay psupf0 u b
693 uzc00 = ?
694 704
695 zc5 : ZChain A f mf ay x 705 zc5 : ZChain A f mf ay x
696 zc5 with ODC.∋-p O A (* x) 706 zc5 with ODC.∋-p O A (* x)
697 ... | no noax = no-extension where -- ¬ A ∋ p, just skip 707 ... | no noax = no-extension where -- ¬ A ∋ p, just skip
698 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f ) 708 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )
699 -- we have to check adding x preserve is-max ZChain A y f mf x 709 -- we have to check adding x preserve is-max ZChain A y f mf x
700 ... | case1 pr = no-extension 710 ... | case1 pr = no-extension
701 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) 711 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
702 ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 712 ... | case1 is-sup = record { initial = ? ; chain∋init = ? ; supf = psupf1 ; chain-mono = ?
713 ; chain⊆A = ? ; f-next = ? ; f-total = ? } where -- x is a sup of (zc ?)
714 psupf1 : Ordinal → Ordinal
715 psupf1 z with trio< z x
716 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
717 ... | tri≈ ¬a b ¬c = x
718 ... | tri> ¬a ¬b c = x
703 ... | case2 ¬x=sup = no-extension -- x is not f y' nor sup of former ZChain from y -- no extention 719 ... | case2 ¬x=sup = no-extension -- x is not f y' nor sup of former ZChain from y -- no extention
704 720
705 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) 721 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)
706 SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A) 722 SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A)
707 723