Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 811:e09ba00c9b85
nvim-agda bug in zorn.agda
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 16 Aug 2022 14:34:54 +0900 |
parents | ae0f958e648b |
children | 96e6643c833d |
comparison
equal
deleted
inserted
replaced
810:ae0f958e648b | 811:e09ba00c9b85 |
---|---|
698 -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x | 698 -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x |
699 | 699 |
700 record xSUP : Set n where | 700 record xSUP : Set n where |
701 field | 701 field |
702 ax : odef A x | 702 ax : odef A x |
703 not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax | 703 is-sup : IsSup A (UnionCF A f mf ay supf0 x) ax |
704 | 704 |
705 UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) → (z0≤px : z0 o≤ px ) → (z1≤x : z1 o≤ x ) | 705 UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) → (z0≤px : z0 o≤ px ) → (z1≤x : z1 o≤ x ) |
706 → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 | 706 → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 |
707 UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ | 707 UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ |
708 UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫ = zc60 fc where | 708 UnionCF⊆ {z0} {z1} z0≤1 z0≤px z1≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫ = zc60 fc where |
736 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ | 736 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ |
737 no-extension : ¬ xSUP → ZChain A f mf ay x | 737 no-extension : ¬ xSUP → ZChain A f mf ay x |
738 no-extension ¬sp=x = record { supf = supf1 ; sup = sup | 738 no-extension ¬sp=x = record { supf = supf1 ; sup = sup |
739 ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf | 739 ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf |
740 ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where | 740 ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where |
741 UnionCFR⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay supf0 x | 741 UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o≤ x → z1 o≤ px → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1 |
742 UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ | 742 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x z1≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ |
743 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ | 743 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x z1≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫ = zc60 fc where |
744 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with | 744 zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w |
745 -- UnionCFR⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ | 745 zc60 {w} (init asp refl) with trio< u1 px | inspect supf1 u1 |
746 -- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ | 746 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) |
747 -- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ | 747 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init asp refl ) ⟫ where |
748 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) | |
749 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc ) | |
750 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → | |
751 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) | |
752 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s | |
753 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
754 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
755 ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px | |
756 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) | |
757 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init asp refl ) ⟫ where | |
758 fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) | |
759 fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc ) | |
760 order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → | |
761 (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) | |
762 order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s | |
763 ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
764 ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) | |
765 ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px | |
766 ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px | |
767 ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) ) | |
768 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) | |
769 ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) | |
770 zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq2} | tri≈ ¬a' b ¬c with osuc-≡< (OrdTrans u1≤x (o≤-refl0 b) ) | |
771 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) | |
772 ... | case2 lt = ⊥-elim ( o<> lt px<u1 ) | |
773 zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq2} | tri> ¬a' ¬b' px<z0 = ⊥-elim ( ¬sp=x zcsup ) where | |
774 zc30 : x ≡ z0 | |
775 zc30 with osuc-≡< z0≤x | |
776 ... | case1 eq = sym (eq) | |
777 ... | case2 z0<x = ⊥-elim (¬p<x<op ⟪ px<z0 , subst (λ k → z0 o< k ) (sym (Oprev.oprev=x op)) z0<x ⟫ ) | |
778 zc31 : x ≡ u1 | |
779 zc31 with trio< x u1 | |
780 ... | tri≈ ¬a b ¬c = b | |
781 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) c ⟫ ) | |
782 zc31 | tri< a ¬b ¬c with osuc-≡< (subst (λ k → u1 o≤ k ) (sym zc30) u1≤x ) -- px<u1 u1≤x, | |
783 ... | case1 u1=x = ⊥-elim ( ¬b (sym u1=x) ) | |
784 ... | case2 u1<x = ⊥-elim ( o<> u1<x a ) | |
785 zc33 : supf1 u1 ≡ u1 -- u1 ≡ supf1 u1 ≡ supf1 x ≡ sp1 | |
786 zc33 = ChainP.supu=u u1-is-sup | |
787 zc32 : sp1 ≡ x | |
788 zc32 = begin | |
789 ? ≡⟨ ? ⟩ | |
790 ? ∎ where open ≡-Reasoning | |
791 zcsup : xSUP | |
792 zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = {!!} } } | |
793 zc60 (fsuc w1 fc) with zc60 fc | |
794 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ | |
795 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ | |
748 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) | 796 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) |
749 sup {z} z≤x with trio< z px | 797 sup {z} z≤x with trio< z px |
750 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ {!!}) ( ZChain.sup zc (o<→≤ a) ) | 798 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z≤x (o<→≤ a)) ( ZChain.sup zc (o<→≤ a) ) |
751 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ {!!}) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )) | 799 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z≤x (o≤-refl0 b)) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )) |
752 ... | tri> ¬a ¬b c = {!!} | 800 ... | tri> ¬a ¬b c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = {!!} } |
753 sup=u : {b : Ordinal} (ab : odef A b) → | 801 sup=u : {b : Ordinal} (ab : odef A b) → |
754 b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b | 802 b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b |
755 sup=u {b} ab b<x is-sup with trio< b px | 803 sup=u {b} ab b≤x is-sup with trio< b px |
756 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) {!!} | 804 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = {!!} } |
757 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) {!!} | 805 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) record { x<sup = {!!} } |
758 ... | tri> ¬a ¬b c = {!!} | 806 ... | tri> ¬a ¬b px<b = {!!} where |
807 zc30 : x ≡ b | |
808 zc30 with osuc-≡< b≤x | |
809 ... | case1 eq = sym (eq) | |
810 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) | |
759 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) | 811 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) |
760 csupf {b} b≤x with trio< b px | 812 csupf {b} b≤x with trio< b px | inspect supf1 b |
761 ... | tri< a ¬b ¬c = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) ) | 813 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) ) |
762 ... | tri≈ ¬a refl ¬c = UnionCF⊆ o≤-refl o≤-refl b≤x ( ZChain.csupf zc o≤-refl ) | 814 ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl b≤x ( ZChain.csupf zc o≤-refl ) |
763 ... | tri> ¬a ¬b px<b = ⟪ {!!} , ch-is-sup b o≤-refl {!!} {!!} ⟫ where | 815 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = |
816 ⟪ SUP.as sup1 , ch-is-sup b o≤-refl zc31 (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl)) ⟫ | |
817 where | |
764 -- px< b ≤ x | 818 -- px< b ≤ x |
765 -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1 | 819 -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1 |
766 zc30 : x ≡ b | 820 zc30 : x ≡ b |
767 zc30 with osuc-≡< b≤x | 821 zc30 with osuc-≡< b≤x |
768 ... | case1 eq = sym (eq) | 822 ... | case1 eq = sym (eq) |
769 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) | 823 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) |
824 zc31 : ChainP A f mf ay supf1 b | |
825 zc31 = record { fcy<sup = {!!} ; order = {!!} ; supu=u = {!!} } | |
770 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) | 826 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) |
771 sis = {!!} | 827 sis {z} z≤x = {!!} |
772 zc4 : ZChain A f mf ay x | 828 zc4 : ZChain A f mf ay x |
773 zc4 with ODC.∋-p O A (* x) | 829 zc4 with ODC.∋-p O A (* x) |
774 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip | 830 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip |
775 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f ) | 831 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f ) |
776 -- we have to check adding x preserve is-max ZChain A y f mf x | 832 -- we have to check adding x preserve is-max ZChain A y f mf x |
789 ... | tri< a ¬b ¬c = ZChain.supf zc z | 845 ... | tri< a ¬b ¬c = ZChain.supf zc z |
790 ... | tri≈ ¬a b ¬c = x | 846 ... | tri≈ ¬a b ¬c = x |
791 ... | tri> ¬a ¬b c = x | 847 ... | tri> ¬a ¬b c = x |
792 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b) | 848 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b) |
793 csupf {b} b≤x with trio< b px | inspect psupf1 b | 849 csupf {b} b≤x with trio< b px | inspect psupf1 b |
794 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫ | 850 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫ |
795 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫ | 851 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ {!!} , {!!} ⟫ |
796 ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!} where -- b ≡ x, supf x ≡ sp | 852 ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!} where -- b ≡ x, supf x ≡ sp |
797 zc30 : x ≡ b | 853 zc30 : x ≡ b |
798 zc30 with trio< x b | 854 zc30 with trio< x b |
799 ... | tri< a ¬b ¬c = ? | 855 ... | tri< a ¬b ¬c = {!!} |
800 ... | tri≈ ¬a b ¬c = ? | 856 ... | tri≈ ¬a b ¬c = {!!} |
801 ... | tri> ¬a ¬b c = ? | 857 ... | tri> ¬a ¬b c = {!!} |
802 | 858 |
803 ... | case2 ¬x=sup = no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention | 859 ... | case2 ¬x=sup = no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention |
804 | 860 |
805 ... | no lim = zc5 where | 861 ... | no lim = zc5 where |
806 | 862 |
880 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal | 936 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal |
881 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z | 937 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z |
882 UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x | 938 UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x |
883 UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ | 939 UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ |
884 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ | 940 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ |
885 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with | 941 UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = {!!} -- with |
886 -- UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ | 942 -- UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ |
887 -- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ | 943 -- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ |
888 -- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ | 944 -- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ |
889 UnionCF0⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay psupf0 x | 945 UnionCFR⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay psupf0 x |
890 UnionCF0⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ | 946 UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ |
891 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ | 947 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ |
892 UnionCF0⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = ? -- with | 948 UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = {!!} -- with |
893 -- UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ | 949 -- UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ |
894 -- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ | 950 -- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ |
895 -- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ | 951 -- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ |
896 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) | 952 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) |
897 sup {z} z≤x with trio< z x | 953 sup {z} z≤x with trio< z x |
898 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} ) | 954 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} ) |
899 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF0⊆ {!!}) usup | 955 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ {!!}) usup |
900 ... | tri> ¬a ¬b c = SUP⊆ (UnionCF0⊆ {!!}) usup | 956 ... | tri> ¬a ¬b c = SUP⊆ (UnionCFR⊆ {!!}) usup |
901 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z)) | 957 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z)) |
902 sis {z} z≤x with trio< z x | 958 sis {z} z≤x with trio< z x |
903 ... | tri< a ¬b ¬c = {!!} where | 959 ... | tri< a ¬b ¬c = {!!} where |
904 zc8 = ZChain.supf-is-sup (pzc z a) o≤-refl | 960 zc8 = ZChain.supf-is-sup (pzc z a) o≤-refl |
905 ... | tri≈ ¬a b ¬c = refl | 961 ... | tri≈ ¬a b ¬c = refl |