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

comparison src/zorn.agda @ 872:a639a0d92659

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 Fri, 16 Sep 2022 20:12:10 +0900
parents 2eaa61279c36
children 27bab3f65064
comparison
equal deleted inserted replaced
871:2eaa61279c36 872:a639a0d92659
50 50
51 -- 51 --
52 -- Partial Order on HOD ( possibly limited in A ) 52 -- Partial Order on HOD ( possibly limited in A )
53 -- 53 --
54 54
55 _<<_ : (x y : Ordinal ) → Set n -- Set n order 55 _<<_ : (x y : Ordinal ) → Set n
56 x << y = * x < * y 56 x << y = * x < * y
57 57
58 _<=_ : (x y : Ordinal ) → Set n -- Set n order 58 _<=_ : (x y : Ordinal ) → Set n -- we can't use * x ≡ * y, it is Set (Level.suc n). Level (suc n) troubles Chain
59 x <= y = (x ≡ y ) ∨ ( * x < * y ) 59 x <= y = (x ≡ y ) ∨ ( * x < * y )
60 60
61 POO : IsStrictPartialOrder _≡_ _<<_ 61 POO : IsStrictPartialOrder _≡_ _<<_
62 POO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 62 POO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
63 ; trans = IsStrictPartialOrder.trans PO 63 ; trans = IsStrictPartialOrder.trans PO
407 ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) 407 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
408 408
409 supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x 409 supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x
410 supf-idem = ? 410 supf-idem = ?
411 411
412 x≤supfx : {x : Ordinal } → x o≤ supf x 412 x≤supfx : (x : Ordinal ) → x o≤ supf x
413 x≤supfx = ? 413 x≤supfx = ?
414 414
415 supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b) 415 supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
416 supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) ) 416 supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
417 417
418 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 418 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
419 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) 419 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)
420 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 420 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
421 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) )) 421 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
422 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt ) 422 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
423 423
424 -- ordering is not proved here but in ZChain1 424 -- ordering is not proved here but in ZChain1
425 425
426 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 426 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
427 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 427 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
591 ; x=fy = HasPrev.x=fy nhp } ) 591 ; x=fy = HasPrev.x=fy nhp } )
592 m05 : ZChain.supf zc b ≡ b 592 m05 : ZChain.supf zc b ≡ b
593 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) 593 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) )
594 ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz ) } , m04 ⟫ 594 ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz ) } , m04 ⟫
595 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b 595 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
596 m08 {z} fcz = ZChain.fcy<sup zc b<A fcz 596 m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
597 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 597 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
598 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b 598 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
599 m09 {s} {z} s<b fcz = order b<A s<b fcz 599 m09 {s} {z} s<b fcz = order b<A s<b fcz
600 m06 : ChainP A f mf ay supf b 600 m06 : ChainP A f mf ay supf b
601 m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 } 601 m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 }
611 ... | case2 y<b = chain-mono1 (osucc b<x) 611 ... | case2 y<b = chain-mono1 (osucc b<x)
612 ⟪ ab , ch-is-sup b <-osuc m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where 612 ⟪ ab , ch-is-sup b <-osuc m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where
613 m09 : b o< & A 613 m09 : b o< & A
614 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) 614 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
615 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b 615 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
616 m07 {z} fc = ZChain.fcy<sup zc m09 fc 616 m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
617 m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 617 m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
618 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b 618 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
619 m08 {s} {z1} s<b fc = order m09 s<b fc 619 m08 {s} {z1} s<b fc = order m09 s<b fc
620 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f 620 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
621 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) 621 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp)
756 -- UninCF supf0 x supf0 px is included 756 -- UninCF supf0 x supf0 px is included
757 -- supf0 px ≡ px 757 -- supf0 px ≡ px
758 -- supf0 px ≡ supf0 x 758 -- supf0 px ≡ supf0 x
759 759
760 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x 760 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x
761 no-extension P with osuc-≡< (ZChain.x≤supfx zc) 761 no-extension P with osuc-≡< (ZChain.x≤supfx zc px)
762 ... | case1 sfpx=px = ? 762 ... | case1 sfpx=px = ? where
763 pchainpx : HOD 763 pchainpx : HOD
764 pchainpx = record { od = record { def = λ z → UChain A f mf ay supf0 z x ∨ FClosure A f px z } ; odmax = & A ; <odmax = zc00 } where 764 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
765 zc00 : {z : Ordinal } → UChain A f mf ay supf0 z x ∨ FClosure A f px z → z o< & A 765 zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A
766 zc00 = ? 766 zc00 {z} (case1 lt) = z07 lt
767 767 zc00 {z} (case2 fc) = z09 ( A∋fc px f mf fc )
768 sup1 : SUP A (pchainpx sfpx=px ) 768 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → odef A z
769 sup1 = supP ? ? ? 769 zc01 {z} (case1 lt) = proj1 lt
770 zc01 {z} (case2 fc) = ( A∋fc px f mf fc )
771
772 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b
773 zc02 {a} {b} ca fb = zc05 fb where
774 zc06 : & (SUP.sup (ZChain.sup zc o≤-refl)) ≡ px
775 zc06 = trans (sym ( ZChain.supf-is-sup zc o≤-refl )) (sym sfpx=px)
776 zc05 : {b : Ordinal } → FClosure A f px b → a <= b
777 zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb ))
778 ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
779 ... | case2 lt = <-ftrans (zc05 fb) (case2 lt)
780 zc05 (init b1 refl) with SUP.x<sup (ZChain.sup zc o≤-refl)
781 (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
782 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 (cong (&) eq))
783 ... | case2 lt = case2 (subst (λ k → (* a) < k ) (trans (sym *iso) (cong (*) zc06)) lt)
784
785 ptotal : IsTotalOrderSet pchainpx
786 ptotal (case1 a) (case1 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso
787 (chain-total A f mf ay supf0 (proj2 a) (proj2 b))
788 ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b
789 ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
790 eq1 : a0 ≡ b0
791 eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
792 ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
793 lt1 : a0 < b0
794 lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
795 ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b
796 ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
797 eq1 : a0 ≡ b0
798 eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
799 ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1 where
800 lt1 : a0 < b0
801 lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
802 ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp px f mf a b)
803
804 sup1 : SUP A pchainpx
805 sup1 = supP pchainpx zc01 ptotal
770 806
771 sp1 : Ordinal 807 sp1 : Ordinal
772 sp1 = & (SUP.sup (sup1 sfpx=px )) 808 sp1 = & (SUP.sup sup1 )
773 809
774 supf1 : Ordinal → Ordinal 810 supf1 : Ordinal → Ordinal
775 supf1 z with trio< z px 811 supf1 z with trio< z px
776 ... | tri< a ¬b ¬c = supf0 z 812 ... | tri< a ¬b ¬c = supf0 z
777 ... | tri≈ ¬a b ¬c = supf0 z 813 ... | tri≈ ¬a b ¬c = px
778 ... | tri> ¬a ¬b c = sp1 sfpx=px 814 ... | tri> ¬a ¬b c = sp1
779 815
780 pchainp : HOD 816 pchainp : HOD
781 pchainp = UnionCF A f mf ay (supfp sfpx=px ) x 817 pchainp = UnionCF A f mf ay supf1 x
782 818
783 819
784 ... | case2 px<spfx = record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 820 ... | case2 px<spfx = record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono
785 ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where 821 ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where
786 822
787 supfp : Ordinal → Ordinal 823 supf1 : Ordinal → Ordinal
788 supfp lt z with trio< z px 824 supf1 z with trio< z px
789 ... | tri< a ¬b ¬c = supf0 z 825 ... | tri< a ¬b ¬c = supf0 z
790 ... | tri≈ ¬a b ¬c = supf0 z 826 ... | tri≈ ¬a b ¬c = supf0 px
791 ... | tri> ¬a ¬b c = supf0 px 827 ... | tri> ¬a ¬b c = supf0 px
792 828
793 pchain1 : (sfpx=px : px o< supfp px ) → HOD 829 pchain1 : HOD
794 pchain1 lt = UnionCF A f mf ay supfp x 830 pchain1 = UnionCF A f mf ay supf1 x
795 831
796 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z 832 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
797 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 833 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
798 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫ 834 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ? ? ⟫
799 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f ) 835 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f )
800 → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z ) 836 → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
801 zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 837 zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
802 zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px 838 zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px
803 ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px u1-is-sup fc ⟫ 839 ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px ? fc ⟫
804 ... | tri≈ ¬a eq ¬c = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 fc ⟫ where 840 ... | tri≈ ¬a eq ¬c = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 ? ⟫ where
805 s1u=u : supf0 u1 ≡ u1 841 s1u=u : supf0 u1 ≡ u1
806 s1u=u = ChainP.supu=u u1-is-sup 842 s1u=u = ? -- ChainP.supu=u u1-is-sup
807 zc12 : supf0 u1 ≡ px 843 zc12 : supf0 u1 ≡ px
808 zc12 = trans (ChainP.supu=u u1-is-sup) eq 844 zc12 = trans s1u=u eq
809 zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where 845 zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where
810 eq : u1 ≡ x 846 eq : u1 ≡ x
811 eq with trio< u1 x 847 eq with trio< u1 x
812 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) 848 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
813 ... | tri≈ ¬a b ¬c = b 849 ... | tri≈ ¬a b ¬c = b
814 ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c ) 850 ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c )
815 s1u=x : supf0 u1 ≡ x 851 s1u=x : supf0 u1 ≡ x
816 s1u=x = trans (ChainP.supu=u u1-is-sup) eq 852 s1u=x = trans ? eq
817 zc13 : osuc px o< osuc u1 853 zc13 : osuc px o< osuc u1
818 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) 854 zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) )
819 x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) 855 x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
820 x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x 856 x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
821 ( ChainP.fcy<sup u1-is-sup {w} fc )
822 x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) zc13 )) 857 x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) zc13 ))
823 ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 (o<→≤ u<x) ) where 858 ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 (o<→≤ u<x) ) where
824 zc14 : u ≡ osuc px 859 zc14 : u ≡ osuc px
825 zc14 = begin 860 zc14 = begin
826 u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ 861 u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩
827 supf0 u ≡⟨ eq1 ⟩ 862 supf0 u ≡⟨ eq1 ⟩
828 supf0 u1 ≡⟨ s1u=x ⟩ 863 supf0 u1 ≡⟨ s1u=x ⟩
829 x ≡⟨ sym (Oprev.oprev=x op) ⟩ 864 x ≡⟨ sym (Oprev.oprev=x op) ⟩
830 osuc px ∎ where open ≡-Reasoning 865 osuc px ∎ where open ≡-Reasoning
831 ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt fc ) 866 ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
832 zc12 : supf0 x ≡ u1 867 zc12 : supf0 x ≡ u1
833 zc12 = subst (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup) 868 zc12 = subst (λ k → supf0 k ≡ u1) eq ?
834 zcsup : xSUP (UnionCF A f mf ay supf0 px) x 869 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
835 zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc) 870 zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc)
836 ; is-sup = record { x<sup = x<sup } } 871 ; is-sup = record { x<sup = x<sup } }
837 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where 872 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where
838 eq : u1 ≡ x 873 eq : u1 ≡ x
839 eq with trio< u1 x 874 eq with trio< u1 x
840 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) 875 ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
841 ... | tri≈ ¬a b ¬c = b 876 ... | tri≈ ¬a b ¬c = b
842 ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c ) 877 ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c )
843 zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z 878 zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z
844 zc20 {z} (init asu su=z ) = zc13 where 879 zc20 {z} (init asu su=z ) = zc13 where
845 zc14 : x ≡ z 880 zc14 : x ≡ z
846 zc14 = begin 881 zc14 = begin
847 x ≡⟨ sym eq ⟩ 882 x ≡⟨ sym eq ⟩
848 u1 ≡⟨ sym (ChainP.supu=u u1-is-sup ) ⟩ 883 u1 ≡⟨ sym ? ⟩
849 supf0 u1 ≡⟨ su=z ⟩ 884 supf0 u1 ≡⟨ su=z ⟩
850 z ∎ where open ≡-Reasoning 885 z ∎ where open ≡-Reasoning
851 zc13 : odef pchain z 886 zc13 : odef pchain z
852 zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) ) 887 zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) )
853 zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 fc) 888 zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 fc)
864 zc30 with osuc-≡< z≤x 899 zc30 with osuc-≡< z≤x
865 ... | case1 eq = eq 900 ... | case1 eq = eq
866 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) 901 ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
867 zc32 = ZChain.sup zc o≤-refl 902 zc32 = ZChain.sup zc o≤-refl
868 zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) 903 zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
869 zc34 ne {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt) 904 zc34 ne {w} lt with zc11 P ?
870 ... | case1 lt = SUP.x<sup zc32 lt 905 ... | case1 lt = SUP.x<sup zc32 lt
871 ... | case2 ⟪ spx=px , fc ⟫ = ⊥-elim ( ne spx=px ) 906 ... | case2 ⟪ spx=px , fc ⟫ = ⊥-elim ( ne spx=px )
872 zc33 : supf0 z ≡ & (SUP.sup zc32) 907 zc33 : supf0 z ≡ & (SUP.sup zc32)
873 zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) 908 zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl )
874 zc36 : ¬ (supf0 px ≡ px) → STMP z≤x 909 zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
891 ... | case1 eq = sym (eq) 926 ... | case1 eq = sym (eq)
892 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) 927 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
893 zcsup : xSUP (UnionCF A f mf ay supf0 px) x 928 zcsup : xSUP (UnionCF A f mf ay supf0 px) x
894 zcsup with zc30 929 zcsup with zc30
895 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 930 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt →
896 IsSup.x<sup (proj1 is-sup) (zc10 lt)} } 931 IsSup.x<sup (proj1 is-sup) ?} }
897 zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b 932 zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
898 zc31 (case1 ¬sp=x) with zc30 933 zc31 (case1 ¬sp=x) with zc30
899 ... | refl = ⊥-elim (¬sp=x zcsup ) 934 ... | refl = ⊥-elim (¬sp=x zcsup )
900 zc31 (case2 hasPrev ) with zc30 935 zc31 (case2 hasPrev ) with zc30
901 ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev 936 ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
902 ; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } ) 937 ; ay = ? ; x=fy = HasPrev.x=fy hasPrev } )
903 938
904 zc4 : ZChain A f mf ay x 939 zc4 : ZChain A f mf ay x
905 zc4 with ODC.∋-p O A (* x) 940 zc4 with ODC.∋-p O A (* x)
906 ... | no noax = no-extension (case1 ( λ s → noax (subst (λ k → odef A k ) (sym &iso) (xSUP.ax s) ))) -- ¬ A ∋ p, just skip 941 ... | no noax = no-extension (case1 ( λ s → noax (subst (λ k → odef A k ) (sym &iso) (xSUP.ax s) ))) -- ¬ A ∋ p, just skip
907 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f ) 942 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) x f )
908 -- we have to check adding x preserve is-max ZChain A y f mf x 943 -- we have to check adding x preserve is-max ZChain A y f mf x
909 ... | case1 pr = no-extension (case2 pr) -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next 944 ... | case1 pr = no-extension (case2 pr) -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
910 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) 945 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
911 ... | case1 is-sup = -- x is a sup of zc 946 ... | case1 is-sup = ? -- x is a sup of zc
912 record { supf = supf1
913 ; sup=u = {!!} ; supf-mono = {!!}
914 ; sup = {!!} ; supf-is-sup = {!!} } where
915
916 supf0px=x : (ax : odef A x) → IsSup A (ZChain.chain zc ) ax → x ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
917 supf0px=x is-sup = ? where
918 zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
919 zc50 = ZChain.supf-is-sup zc ?
920
921 pchain⊆x : UnionCF A f mf ay supf0 px ⊆' UnionCF A f mf ay supf1 x
922 pchain⊆x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
923 pchain⊆x ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ au , ch-is-sup u ? ? ? ⟫
924
925 supfx1 : {z : Ordinal } → x o≤ z → supf1 z ≡ x
926 supfx1 {z} x≤z with trio< z px
927 ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
928 ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
929 ... | tri> ¬a ¬b c = refl
930
931 pchain0=x : UnionCF A f mf ay supf0 px ≡ UnionCF A f mf ay supf1 px
932 pchain0=x = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
933 zc10 : {z : Ordinal} → OD.def (od pchain) z → odef (UnionCF A f mf ay supf1 px) z
934 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
935 zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ? ⟫
936 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 px) z → OD.def (od pchain) z
937 zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
938 zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ?
939
940
941 ... | case2 ¬x=sup = no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention 947 ... | case2 ¬x=sup = no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention
942 nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x 948 nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x
943 nsup s = ¬x=sup z12 where 949 nsup s = ¬x=sup z12 where
944 z12 : IsSup A (UnionCF A f mf ay supf0 px) ax 950 z12 : IsSup A (UnionCF A f mf ay supf0 px) ax
945 z12 = record { x<sup = λ {z} lt → subst (λ k → (z ≡ k) ∨ (z << k )) (sym &iso) ( IsSup.x<sup ( xSUP.is-sup s ) lt ) } 951 z12 = record { x<sup = λ {z} lt → subst (λ k → (z ≡ k) ∨ (z << k )) (sym &iso) ( IsSup.x<sup ( xSUP.is-sup s ) lt ) }