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

comparison src/zorn.agda @ 682:663b34227faf

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 Sat, 09 Jul 2022 21:51:39 +0900
parents c5c8e37d9a6c
children 6814fc4e7998
comparison
equal deleted inserted replaced
681:c5c8e37d9a6c 682:663b34227faf
463 ... | case2 ¬x=sup = ? 463 ... | case2 ¬x=sup = ?
464 464
465 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 465 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
466 → (zc0 : (x : Ordinal) → ZChain1 A f mf ay x) 466 → (zc0 : (x : Ordinal) → ZChain1 A f mf ay x)
467 → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x 467 → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x
468 ind f mf {y} ay x zc0 prev = zc4 where 468 ind f mf {y} ay x zc0 prev with Oprev-p x
469 zc : {z1 : Ordinal} → z1 o< x → ZChain A f mf ay zc0 z1 469 ... | yes op = ? where
470 zc z1 with Oprev-p x 470 --
471 ... | yes op = ? where 471 -- we have previous ordinal to use induction
472 -- 472 --
473 -- we have previous ordinal to use induction 473 px = Oprev.oprev op
474 -- 474 supf : Ordinal → HOD
475 px = Oprev.oprev op 475 supf x = ? -- ChainF A f mf ay x zc0
476 supf : Ordinal → HOD 476 zc : ZChain A f mf ay zc0 (Oprev.oprev op)
477 supf x = ? -- ChainF A f mf ay x zc0 477 zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
478 -- zc : ZChain A f mf ay zc0 (Oprev.oprev op) 478 px<x : px o< x
479 -- zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 479 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
480 px<x : px o< x
481 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
482 ... | no ¬ox = ? where
483 supf : Ordinal → HOD
484 supf x = ? -- Z?Chain1.chain zc0
485 uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf ay zc0 (UChain.u u)
486 uzc {z} u = prev (UChain.u u) (UChain.u<x u)
487 Uz : HOD
488 Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!} }
489
490 -- if previous chain satisfies maximality, we caan reuse it 480 -- if previous chain satisfies maximality, we caan reuse it
491 -- 481 --
492 no-extenion : ( {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x )) a → b o< osuc x → (ab : odef A b) → 482 no-extenion : ( {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain ?) a → b o< osuc x → (ab : odef A b) →
493 HasPrev A (ZChain.chain (zc z<x) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) ) ab → 483 HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain ? ) ab →
494 * a < * b → odef (ZChain.chain (zc ?) ) b ) → ZChain A f mf ay zc0 x 484 * a < * b → odef (ZChain.chain zc ) b ) → ZChain A f mf ay zc0 x
495 no-extenion is-max = ? 485 no-extenion is-max = ?
496 486
497 zc4 : ZChain A f mf ay zc0 x 487 zc4 : ZChain A f mf ay zc0 x
498 zc4 with o≤? x o∅ 488 zc4 with o≤? x o∅
499 ... | yes x=0 = ? 489 ... | yes x=0 = ?
500 ... | no 0<x with ODC.∋-p O A (* x) 490 ... | no 0<x with ODC.∋-p O A (* x)
501 ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip 491 ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip
502 zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) → 492 zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
503 HasPrev A (ZChain.chain (zc ?) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) ) ab → 493 HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
504 * a < * b → odef (ZChain.chain (zc z<x) ) b 494 * a < * b → odef (ZChain.chain zc ) b
505 zc1 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox 495 zc1 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
506 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) ) 496 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
507 ... | case2 lt = ZChain.is-max (zc z<x) za ? ab P a<b 497 ... | case2 lt = ZChain.is-max zc za ? ab P a<b
508 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain (zc ? ) ) ax f ) 498 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )
509 -- we have to check adding x preserve is-max ZChain A y f mf zc0 x 499 -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
510 ... | case1 pr = no-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next 500 ... | case1 pr = no-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
511 chain0 = ZChain.chain (zc ? ) 501 chain0 = ZChain.chain zc
512 zc7 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) → 502 zc7 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
513 HasPrev A (ZChain.chain (zc z<x) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) ) ab → 503 HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
514 * a < * b → odef (ZChain.chain (zc z<x) ) b 504 * a < * b → odef (ZChain.chain zc ) b
515 zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox 505 zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
516 ... | case2 lt = ZChain.is-max (zc z<x) za ? ab P a<b 506 ... | case2 lt = ZChain.is-max zc za ? ab P a<b
517 ... | case1 b=x = ? -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next (zc z<x) (HasPrev.ay pr)) 507 ... | case1 b=x = ? -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
518 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain (zc ?) ) ax ) 508 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
519 ... | case1 is-sup = -- x is a sup of (zc ?) 509 ... | case1 is-sup = -- x is a sup of zc
520 record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} 510 record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!}
521 ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where 511 ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where
522 sup0 : SUP A (ZChain.chain (zc ?) ) 512 sup0 : SUP A (ZChain.chain zc )
523 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where 513 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
524 x21 : {y : HOD} → ZChain.chain (zc ?) ∋ y → (y ≡ * x) ∨ (y < * x) 514 x21 : {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x)
525 x21 {y} zy with IsSup.x<sup is-sup zy 515 x21 {y} zy with IsSup.x<sup is-sup zy
526 ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) ) 516 ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) )
527 ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x ) 517 ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x )
528 sp : HOD 518 sp : HOD
529 sp = SUP.sup sup0 519 sp = SUP.sup sup0
530 x=sup : x ≡ & sp 520 x=sup : x ≡ & sp
531 x=sup = sym &iso 521 x=sup = sym &iso
532 chain0 = ZChain.chain (zc ?) 522 chain0 = ZChain.chain zc
533 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A 523 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
534 sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A (zc ?) (subst (λ k → odef chain0 k) (sym &iso) zx ))) 524 sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc (subst (λ k → odef chain0 k) (sym &iso) zx )))
535 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) ) 525 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
536 schain : HOD 526 schain : HOD
537 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy } 527 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy }
538 supf0 : Ordinal → HOD 528 supf0 : Ordinal → HOD
539 supf0 z with trio< z x 529 supf0 z with trio< z x
540 ... | tri< a ¬b ¬c = ? -- supf z 530 ... | tri< a ¬b ¬c = ? -- supf z
541 ... | tri≈ ¬a b ¬c = schain 531 ... | tri≈ ¬a b ¬c = schain
542 ... | tri> ¬a ¬b c = schain 532 ... | tri> ¬a ¬b c = schain
543 A∋schain : {x : HOD } → schain ∋ x → A ∋ x 533 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
544 A∋schain (case1 zx ) = ZChain.chain⊆A (zc ?) zx 534 A∋schain (case1 zx ) = ZChain.chain⊆A zc zx
545 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 535 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx
546 s⊆A : schain ⊆' A 536 s⊆A : schain ⊆' A
547 s⊆A {x} (case1 zx) = ZChain.chain⊆A (zc ?) zx 537 s⊆A {x} (case1 zx) = ZChain.chain⊆A zc zx
548 s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx 538 s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx
549 cmp : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a ) 539 cmp : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
550 cmp {a} {b} za fb with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb 540 cmp {a} {b} za fb with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb
551 ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where 541 ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where
552 eq : a ≡ b 542 eq : a ≡ b
559 a<b = subst (λ k → a < k ) (trans sp=b *iso ) (subst (λ k → a < k ) (sym *iso) a<sp ) 549 a<b = subst (λ k → a < k ) (trans sp=b *iso ) (subst (λ k → a < k ) (sym *iso) a<sp )
560 ... | case2 a<sp | case2 sp<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where 550 ... | case2 a<sp | case2 sp<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where
561 a<b : a < b 551 a<b : a < b
562 a<b = ptrans (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b ) 552 a<b = ptrans (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
563 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a ) 553 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
564 scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total (zc ?) {px} {px} o≤-refl za zb 554 scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total zc {px} {px} o≤-refl za zb
565 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb 555 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb
566 scmp (case2 fa) (case1 zb) with cmp zb fa 556 scmp (case2 fa) (case1 zb) with cmp zb fa
567 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq)) a 557 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq)) a
568 ... | tri≈ ¬a b ¬c = tri≈ ¬c (sym b) ¬a 558 ... | tri≈ ¬a b ¬c = tri≈ ¬c (sym b) ¬a
569 ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq)) ¬a 559 ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq)) ¬a
570 scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb) 560 scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb)
571 scnext : {a : Ordinal} → odef schain a → odef schain (f a) 561 scnext : {a : Ordinal} → odef schain a → odef schain (f a)
572 scnext {x} (case1 zx) = case1 (ZChain.f-next (zc ?) zx) 562 scnext {x} (case1 zx) = case1 (ZChain.f-next zc zx)
573 scnext {x} (case2 sx) = case2 ( fsuc x sx ) 563 scnext {x} (case2 sx) = case2 ( fsuc x sx )
574 scinit : {x : Ordinal} → odef schain x → * y ≤ * x 564 scinit : {x : Ordinal} → odef schain x → * y ≤ * x
575 scinit {x} (case1 zx) = ZChain.initial (zc ?) zx 565 scinit {x} (case1 zx) = ZChain.initial zc zx
576 scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init (zc ?) ) ) 566 scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init zc ) )
577 ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) ) 567 ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) )
578 ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp ) 568 ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp )
579 ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x ) 569 ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x )
580 ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) ) 570 ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) )
581 A∋za : {a : Ordinal } → odef chain0 a → odef A a 571 A∋za : {a : Ordinal } → odef chain0 a → odef A a
582 A∋za za = ZChain.chain⊆A (zc ?) za 572 A∋za za = ZChain.chain⊆A zc za
583 za<sup : {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨ ( * a < sp ) 573 za<sup : {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨ ( * a < sp )
584 za<sup za = SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za ) 574 za<sup za = SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za )
585 s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b) 575 s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b)
586 → HasPrev A schain ab f ∨ IsSup A schain ab 576 → HasPrev A schain ab f ∨ IsSup A schain ab
587 → * a < * b → odef schain b 577 → * a < * b → odef schain b
588 s-ismax {a} {b} sa b<ox ab p a<b with osuc-≡< b<ox -- b is x? 578 s-ismax {a} {b} sa b<ox ab p a<b with osuc-≡< b<ox -- b is x?
589 ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) )) 579 ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
590 s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where -- has previous 580 s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where -- has previous
591 z21 : HasPrev A schain ab f → odef schain b 581 z21 : HasPrev A schain ab f → odef schain b
592 z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 582 z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } =
593 case1 (ZChain.is-max (zc ?) za ? ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b ) 583 case1 (ZChain.is-max zc za ? ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
594 z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) ) 584 z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
595 s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max (zc ?) za ? ab (case2 z22) a<b ) where -- previous sup 585 s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc za ? ab (case2 z22) a<b ) where -- previous sup
596 z22 : IsSup A (ZChain.chain (zc ?) ) ab 586 z22 : IsSup A (ZChain.chain zc ) ab
597 z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } 587 z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
598 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p) a<b | case2 b<x with HasPrev.ay p 588 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p) a<b | case2 b<x with HasPrev.ay p
599 ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next (zc ?) zy )) -- in previous closure of f 589 ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc zy )) -- in previous closure of f
600 ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy )) -- in current closure of f 590 ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy )) -- in current closure of f
601 s-ismax {a} {b} (case2 sa) b<ox ab (case2 p) a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc 591 s-ismax {a} {b} (case2 sa) b<ox ab (case2 p) a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc
602 z24 : IsSup A schain ab → IsSup A (ZChain.chain (zc ?) ) ab 592 z24 : IsSup A schain ab → IsSup A (ZChain.chain zc ) ab
603 z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } 593 z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
604 z23 : odef chain0 b 594 z23 : odef chain0 b
605 z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init (zc ?) ) 595 z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc )
606 ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋init (zc ?) ) 596 ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋init zc )
607 ... | case2 y<b = ZChain.is-max (zc ?) (ZChain.chain∋init (zc ?) ) ? ab (case2 (z24 p)) y<b 597 ... | case2 y<b = ZChain.is-max zc (ZChain.chain∋init zc ) ? ab (case2 (z24 p)) y<b
608 seq : schain ≡ supf0 x 598 seq : schain ≡ supf0 x
609 seq with trio< x x 599 seq with trio< x x
610 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) 600 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
611 ... | tri≈ ¬a b ¬c = refl 601 ... | tri≈ ¬a b ¬c = refl
612 ... | tri> ¬a ¬b c = refl 602 ... | tri> ¬a ¬b c = refl
615 ... | tri< a ¬b ¬c = refl 605 ... | tri< a ¬b ¬c = refl
616 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) 606 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x )
617 ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) 607 ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x )
618 608
619 ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention 609 ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
620 z18 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) → 610 z18 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
621 HasPrev A (ZChain.chain (zc ?) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) ) ab → 611 HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
622 * a < * b → odef (ZChain.chain (zc z<x) ) b 612 * a < * b → odef (ZChain.chain zc ) b
623 z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x 613 z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x
624 ... | case2 lt = ZChain.is-max (zc z<x) za ? ab p a<b 614 ... | case2 lt = ZChain.is-max zc za ? ab p a<b
625 ... | case1 b=x with p 615 ... | case1 b=x with p
626 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = ? ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } ) 616 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = ? ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
627 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 617 ... | case2 b=sup = ⊥-elim ( ¬x=sup record {
628 x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup ? ) } ) 618 x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup ? ) } )
619 ... | no op = zc5 where
620 supf : (z : Ordinal ) → z o< x → HOD
621 supf x lt = ZChain1.chainf ( zc0 (& A) ) x
622 uzc : {z : Ordinal} → (u : UChain x supf z) → ZChain A f mf ay zc0 (UChain.u u)
623 uzc {z} u = prev (UChain.u u) (UChain.u<x u)
624 Uz : HOD
625 Uz = record { od = record { def = λ z → odef A z ∧ ( UChain x supf z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!} }
626 zc5 : ZChain A f mf ay zc0 x
627 zc5 with o≤? x o∅
628 ... | yes x=0 = ?
629 ... | no 0<x with ODC.∋-p O A (* x)
630 ... | no noax = ? where -- ¬ A ∋ p, just skip
631 ... | yes ax with ODC.p∨¬p O ( HasPrev A Uz ax f )
632 -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
633 ... | case1 pr = ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
634 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A Uz ax )
635 ... | case1 is-sup = ? -- x is a sup of (zc ?)
636 ... | case2 ¬x=sup = ? -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
637
629 638
630 SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x 639 SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x
631 SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x 640 SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x
632 641
633 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (SZ0 f mf ay ) (& A) 642 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (SZ0 f mf ay ) (& A)