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

comparison src/zorn.agda @ 815:d70f3f0681ea

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 Tue, 16 Aug 2022 21:54:03 +0900
parents 95db436cce67
children 648131d2b83c
comparison
equal deleted inserted replaced
814:95db436cce67 815:d70f3f0681ea
801 zcsup : xSUP 801 zcsup : xSUP
802 zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = zc34 } } 802 zcsup = record { ax = subst (λ k → odef A k) zc32 asp ; is-sup = record { x<sup = zc34 } }
803 zc60 (fsuc w1 fc) with zc60 fc 803 zc60 (fsuc w1 fc) with zc60 fc
804 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 804 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
805 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 805 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫
806 chp10 : {u : Ordinal } → u o< x → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u
807 chp10 = ?
808 fc10 : {w : Ordinal } → u o< x → FClosure A f supf1 w → FClosure A f supf0 w
809 fc10 = ?
806 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z) 810 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
807 sup {z} z<x with trio< z px 811 sup {z} z<x with trio< z px
808 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ? (o<→≤ a)) ( ZChain.sup zc a ) 812 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl (ordtrans z<x <-osuc) (o<→≤ a)) ( ZChain.sup zc a )
809 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where 813 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = λ {w} lt → zc61 (subst (λ k → UnionCF A f mf ay supf1 k ∋ w) b lt) } where
810 zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1) 814 zc61 : {w : HOD} → UnionCF A f mf ay supf1 px ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
811 zc61 {w} lt = ? 815 zc61 {w} ⟪ au , ch-init fc ⟫ with SUP.x<sup sup1 ⟪ au , ch-init fc ⟫
816 ... | case1 eq = case1 eq
817 ... | case2 lt = case2 lt
818 zc61 {w} ⟪ au , ch-is-sup u u≤px is-sup fc ⟫ with SUP.x<sup sup1 ⟪ au , ch-is-sup u (subst (λ k → u o≤ k) (Oprev.oprev=x op) (ordtrans u≤px <-osuc)) ? ? ⟫
819 ... | case1 eq = case1 eq
820 ... | case2 lt = case2 lt
812 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) 821 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
813 sup=u : {b : Ordinal} (ab : odef A b) → 822 sup=u : {b : Ordinal} (ab : odef A b) →
814 b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b 823 b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
815 sup=u {b} ab b≤x is-sup with trio< b px 824 sup=u {b} ab b≤x is-sup with trio< b px
816 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = {!!} } 825 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = {!!} }
817 ... | tri≈ ¬a b ¬c = ? 826 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab {!!} record { x<sup = {!!} }
818 ... | tri> ¬a ¬b px<b = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) ? ⟫ ) 827 ... | tri> ¬a ¬b px<b = {!!} where
828 zc30 : x ≡ b
829 zc30 with osuc-≡< b≤x
830 ... | case1 eq = sym (eq)
831 ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
819 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) 832 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
820 csupf {b} b≤x with trio< b px | inspect supf1 b 833 csupf {b} b≤x with trio< b px | inspect supf1 b
821 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) ) 834 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
822 ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl b≤x ( ZChain.csupf zc o≤-refl ) 835 ... | tri≈ ¬a refl ¬c | _ = UnionCF⊆ o≤-refl o≤-refl b≤x ( ZChain.csupf zc o≤-refl )
823 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = 836 ... | tri> ¬a ¬b px<b | record { eq = eq1 } =
958 -- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ 971 -- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
959 -- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 972 -- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
960 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z) 973 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
961 sup {z} z≤x with trio< z x 974 sup {z} z≤x with trio< z x
962 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} ) 975 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} )
963 ... | tri≈ ¬a b ¬c = ? 976 ... | tri≈ ¬a b ¬c = {!!}
964 ... | tri> ¬a ¬b c = ? 977 ... | tri> ¬a ¬b c = {!!}
965 sis : {z : Ordinal} (x≤z : z o< x) → supf1 z ≡ & (SUP.sup (sup ?)) 978 sis : {z : Ordinal} (x≤z : z o< x) → supf1 z ≡ & (SUP.sup (sup {!!}))
966 sis {z} z<x with trio< z x 979 sis {z} z<x with trio< z x
967 ... | tri< a ¬b ¬c = {!!} where 980 ... | tri< a ¬b ¬c = {!!} where
968 zc8 = ZChain.supf-is-sup (pzc z a) ? 981 zc8 = ZChain.supf-is-sup (pzc z a) {!!}
969 ... | tri≈ ¬a b ¬c = ? 982 ... | tri≈ ¬a b ¬c = {!!}
970 ... | tri> ¬a ¬b c = ? 983 ... | tri> ¬a ¬b c = {!!}
971 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b 984 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
972 sup=u {b} ab b<x is-sup with trio< b x 985 sup=u {b} ab b<x is-sup with trio< b x
973 ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b) (ob<x lim a)) ab {!!} record { x<sup = {!!} } 986 ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b) (ob<x lim a)) ab {!!} record { x<sup = {!!} }
974 ... | tri≈ ¬a b ¬c = {!!} 987 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?) ?) ab {!!} record { x<sup = {!!} }
975 ... | tri> ¬a ¬b c = {!!} 988 ... | tri> ¬a ¬b c = {!!}
976 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z) 989 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
977 csupf {z} z≤x with trio< z x 990 csupf {z} z≤x with trio< z x
978 ... | tri< a ¬b ¬c = zc9 where 991 ... | tri< a ¬b ¬c = zc9 where
979 zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) 992 zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z)