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

comparison src/zorn.agda @ 902:49594badc9b4

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 Sun, 09 Oct 2022 19:30:41 +0900
parents 6146d75131f5
children 5b6034ad8b98
comparison
equal deleted inserted replaced
901:6146d75131f5 902:49594badc9b4
826 -- supf0 px is included by the chain 826 -- supf0 px is included by the chain
827 -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 827 -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x
828 -- supf1 x ≡ sp1, which is not included now 828 -- supf1 x ≡ sp1, which is not included now
829 829
830 pchainpx : HOD 830 pchainpx : HOD
831 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 831 pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z )
832 zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A 832 ∨ FClosure A f (supf0 px) z } ; odmax = & A ; <odmax = zc00 } where
833 zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A
833 zc00 {z} (case1 lt) = z07 lt 834 zc00 {z} (case1 lt) = z07 lt
834 zc00 {z} (case2 fc) = z09 ( A∋fc px f mf fc ) 835 zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc )
835 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → odef A z 836 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → odef A z
836 zc01 {z} (case1 lt) = proj1 lt 837 zc01 {z} (case1 lt) = proj1 lt
837 zc01 {z} (case2 fc) = ( A∋fc px f mf fc ) 838 zc01 {z} (case2 fc) = ( A∋fc (supf0 px) f mf fc )
838 839
839 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b 840 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b
840 zc02 {a} {b} ca fb = zc05 fb where 841 zc02 {a} {b} ca fb = zc05 fb where
841 zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px 842 zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px
842 zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) ? 843 zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) ?
843 zc05 : {b : Ordinal } → FClosure A f px b → a <= b 844 zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b
844 zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb )) 845 zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
845 ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) 846 ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
846 ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 847 ... | case2 lt = <-ftrans (zc05 fb) (case2 lt)
847 zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) ? -- 848 zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) ? --
848 -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca ) 849 -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca )
849 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) 850 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
932 m = ZChain.minsup zc (o≤-refl0 b) 933 m = ZChain.minsup zc (o≤-refl0 b)
933 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 934 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
934 ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } 935 ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z }
935 936
936 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 937 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
937 csupf1 {z1} sz1<x with trio< (supf0 z1) px 938 csupf1 {z1} sz1<x with trio< (supf1 z1) px
938 ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) ? (sym (sf1=sf0 (o<→≤ a) )) (case1 (ZChain.csupf zc a )) where 939 ... | tri< a ¬b ¬c = csupf0 where
939 z1≤px : z1 o≤ px 940 zc18 : supf1 z1 ≡ supf0 z1
940 z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) ? a )) 941 zc18 = sf1=sf0 ?
941 ... | tri≈ ¬a b ¬c = ? 942 csupf0 : odef (UnionCF A f mf ay supf1 x) (supf1 z1)
942 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc21 , subst (λ k → z1 o< k ) (sym (Oprev.oprev=x op)) zc22 ⟫ ) where 943 csupf0 with ZChain.csupf zc (subst (λ k → k o< px) zc18 a )
943 zc21 : px o< z1 944 ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , ch-init ? ⟫
944 zc21 = ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) ? c ) 945 ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab ,
945 zc22 : z1 o< x -- c : px o< supf0 z1 946 ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ? ? ⟫
946 zc22 = ? -- supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? ) 947 ... | tri≈ ¬a b ¬c = ⟪ asm , ch-is-sup (supf1 z1) sz1<x ? (init asm1 ? ) ⟫ where
947 -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x 948 asm : odef A (supf1 z1)
949 asm = subst (λ k → odef A k ) ? ( MinSUP.asm sup1)
950 asm1 : odef A (supf1 (supf1 z1))
951 asm1 = subst (λ k → odef A k ) ? ( MinSUP.asm sup1)
952 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫ )
948 953
949 zc4 : ZChain A f mf ay x --- supf px ≤ supf x 954 zc4 : ZChain A f mf ay x --- supf px ≤ supf x
950 zc4 with trio< x (supf0 px) 955 zc4 with trio< x (supf0 px)
951 ... | tri> ¬a ¬b c = zc41 (o<→≤ c) 956 ... | tri> ¬a ¬b c = zc41 (o<→≤ c)
952 ... | tri≈ ¬a b ¬c = zc41 (o≤-refl0 (sym b)) 957 ... | tri≈ ¬a b ¬c = zc41 (o≤-refl0 (sym b))