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

comparison src/zorn.agda @ 967:cd0ef83189c5

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, 05 Nov 2022 18:29:21 +0900
parents 39c680188738
children 9a8041a7f3c9
comparison
equal deleted inserted replaced
966:39c680188738 967:cd0ef83189c5
857 857
858 sup1 : MinSUP A pchainpx 858 sup1 : MinSUP A pchainpx
859 sup1 = minsupP pchainpx pcha ptotal 859 sup1 = minsupP pchainpx pcha ptotal
860 sp1 = MinSUP.sup sup1 860 sp1 = MinSUP.sup sup1
861 861
862 sfpx<sp1 : supf0 px <= sp1
863 sfpx<sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
864
862 -- 865 --
863 -- supf0 px o≤ sp1 866 -- supf0 px o≤ sp1
864 -- 867 --
865 868
869 --- x ≦ supf px ≦ x ≦ sp ≦ x
870 -- x may apper any place
871
872 -- x < sp → supf x = supf px
873 -- x ≡ sp → supf x = sp
874 -- sp < x → supf x = sp ≡ supf px
875 -- UnionCF A f mf ay supf px ⊆ UnionCF A f mf ay supf x
876
877 -- supf x does not affect UnionCF A f mf ay supf x
878
879 -- supf px < px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
880 -- supf px ≡ px → UnionCF A f mf ay supf px ⊂ UnionCF A f mf ay supf x ≡ pchainx
881 -- x < supf px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
882
883 zc43 : ( x o< sp1 ) ∨ ( sp1 o≤ x )
884 zc43 = ?
885
866 zc41 : ZChain A f mf ay x 886 zc41 : ZChain A f mf ay x
867 zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) 887 zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
868 zc41 | (case2 sfpx<sp1) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? 888 zc41 | (case2 sfpx<sp1) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
869 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where 889 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where
870 -- supf0 px is included by the chain of sp1 890 -- supf0 px is included by the chain of sp1
921 941
922 fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z 942 fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z
923 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc 943 fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
924 fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z 944 fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z
925 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc 945 fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
946
926 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z 947 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z
927 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 948 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
928 zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where 949 zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where
929 u<x : u o< x 950 u<x : u o< x
930 u<x = supf-inject0 supf1-mono su<sx 951 u<x = supf-inject0 supf1-mono su<sx
950 zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px 971 zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px
951 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) 972 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
952 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc ) 973 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc )
953 ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b ))) 974 ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b )))
954 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) 975 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ )
955 zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z 976
956 zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ 977 zc12 : {z : Ordinal} → supf0 px ≡ px → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
957 zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where 978 zc12 {z} sfpx=px (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
979 zc12 {z} sfpx=px (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
958 u<px : u o< px 980 u<px : u o< px
959 u<px = ZChain.supf-inject zc su<sx 981 u<px = ZChain.supf-inject zc su<sx
960 u<x : u o< x 982 u<x : u o< x
961 u<x = ordtrans u<px px<x 983 u<x = ordtrans u<px px<x
962 u≤px : u o≤ px 984 u≤px : u o≤ px
999 zc19 : supf1 px ≡ supf0 u 1021 zc19 : supf1 px ≡ supf0 u
1000 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) 1022 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
1001 s≤px : s o≤ px 1023 s≤px : s o≤ px
1002 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) 1024 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
1003 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ ) 1025 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ )
1004 zc12 {z} (case2 fc) = zc21 fc where 1026 zc12 {z} sfpx=px (case2 fc) = zc21 fc where
1005 --- supf0 px o< sp1 1027 --- supf0 px o< sp1
1006 zc20 : (supf0 px ≡ px ) ∨ ( supf0 px o< px )
1007 zc20 = ?
1008 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 1028 zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
1009 zc21 {z1} (fsuc z2 fc ) with zc21 fc 1029 zc21 {z1} (fsuc z2 fc ) with zc21 fc
1010 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 1030 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
1011 ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 1031 ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
1012 zc21 (init asp refl ) with zc20 1032 zc21 (init asp refl ) = ⟪ asp , ch-is-sup px zc18
1013 ... | case1 sfpx=px = ⟪ asp , ch-is-sup px zc18
1014 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where 1033 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
1015 zc15 : supf1 px ≡ px 1034 zc15 : supf1 px ≡ px
1016 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) 1035 zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
1017 zc18 : supf1 px o< supf1 x 1036 zc18 : supf1 px o< supf1 x
1018 zc18 = ? 1037 zc18 = ?
1033 sf<px : supf0 s o< px 1052 sf<px : supf0 s o< px
1034 sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx 1053 sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx
1035 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 1054 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
1036 csupf17 (init as refl ) = ZChain.csupf zc sf<px 1055 csupf17 (init as refl ) = ZChain.csupf zc sf<px
1037 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) 1056 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
1038
1039 ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px)
1040 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫
1041 ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u zc18
1042 record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫ where
1043 z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
1044 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc)
1045 z11 : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1
1046 → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u )
1047 z11 {s} {z} lt fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? ))
1048 (ChainP.order is-sup lt0 (fcup fc s≤px )) where
1049 s<u : s o< u
1050 s<u = supf-inject0 supf1-mono lt
1051 s≤px : s o≤ px
1052 s≤px = ordtrans s<u ? -- (o<→≤ u<x)
1053 lt0 : supf0 s o< supf0 u
1054 lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt
1055 z12 : supf1 u ≡ u
1056 z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup)
1057 zc18 : supf1 u o< supf1 x
1058 zc18 = ?
1059
1060 1057
1061 1058
1062 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where 1059 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
1063 field 1060 field
1064 tsup : MinSUP A (UnionCF A f mf ay supf1 z) 1061 tsup : MinSUP A (UnionCF A f mf ay supf1 z)
1099 psz1≤px : supf1 z1 o≤ px 1096 psz1≤px : supf1 z1 o≤ px
1100 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x 1097 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x
1101 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) 1098 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1102 csupf2 with trio< z1 px | inspect supf1 z1 1099 csupf2 with trio< z1 px | inspect supf1 z1
1103 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px 1100 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
1104 ... | case2 lt = zc12 (case1 cs03) where 1101 ... | case2 lt = zc12 ? (case1 cs03) where
1105 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) 1102 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
1106 cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) 1103 cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
1107 ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) 1104 ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) )
1108 ... | case1 sfz=sfpx = zc12 (case2 (init (ZChain.asupf zc) cs04 )) where 1105 ... | case1 sfz=sfpx = zc12 ? (case2 (init (ZChain.asupf zc) cs04 )) where
1109 supu=u : supf1 (supf1 z1) ≡ supf1 z1 1106 supu=u : supf1 (supf1 z1) ≡ supf1 z1
1110 supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx) 1107 supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx)
1111 cs04 : supf0 px ≡ supf0 z1 1108 cs04 : supf0 px ≡ supf0 z1
1112 cs04 = begin 1109 cs04 = begin
1113 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ 1110 supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩
1118 --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x 1115 --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x
1119 cs05 : px o< supf0 px 1116 cs05 : px o< supf0 px
1120 cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx 1117 cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
1121 cs06 : supf0 px o< osuc px 1118 cs06 : supf0 px o< osuc px
1122 cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ? 1119 cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ?
1123 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) 1120 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
1124 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? 1121 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ?
1125 -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) 1122 -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
1126 1123
1127 1124
1128 zc41 | (case1 sfp=sp1 ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? 1125 zc41 | (case1 sfp=sp1 ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?