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

comparison src/zorn.agda @ 887:09915b6b4212

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 Mon, 03 Oct 2022 01:43:00 +0900
parents 7c4b65fcba97
children 49e0ab5e30e0
comparison
equal deleted inserted replaced
886:7c4b65fcba97 887:09915b6b4212
1040 u ≡⟨ b ⟩ 1040 u ≡⟨ b ⟩
1041 px ∎ where open ≡-Reasoning 1041 px ∎ where open ≡-Reasoning
1042 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → 1042 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
1043 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) 1043 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
1044 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) 1044 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl)))
1045 ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) ? ss<spx) (fcup fc s≤px) ) where 1045 ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where
1046 zc19 : supf1 px ≡ supf0 u
1047 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
1046 s≤px : s o≤ px 1048 s≤px : s o≤ px
1047 s≤px = ? 1049 s≤px = o<→≤ (supf-inject0 supf-mono1 ss<spx)
1048 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , (ordtrans u<x <-osuc ) ⟫ ) 1050 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , (ordtrans u<x <-osuc ) ⟫ )
1049 zc12 {z} (case2 fc) = zc21 fc where 1051 zc12 {z} (case2 fc) = zc21 fc where
1050 zc21 : {z1 : Ordinal } → FClosure A f px z1 → odef (UnionCF A f mf ay supf1 x) z1 1052 zc21 : {z1 : Ordinal } → FClosure A f px z1 → odef (UnionCF A f mf ay supf1 x) z1
1051 zc21 {z1} (fsuc z2 fc ) with zc21 fc 1053 zc21 {z1} (fsuc z2 fc ) with zc21 fc
1052 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ 1054 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫
1059 zc14 = init (subst (λ k → odef A k) (sym zc15) asp) zc15 1061 zc14 = init (subst (λ k → odef A k) (sym zc15) asp) zc15
1060 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) 1062 zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
1061 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) 1063 zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc )
1062 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → 1064 zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
1063 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) 1065 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
1064 zc17 {s} {z1} ss<spx fc = ? 1066 zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx
1067 (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
1068 mins : MinSUP A (UnionCF A f mf ay supf0 px)
1069 mins = ZChain.minsup zc o≤-refl
1070 mins-is-spx : MinSUP.sup mins ≡ supf1 px
1071 mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
1072 s<px : s o< px
1073 s<px = supf-inject0 supf-mono1 ss<spx
1074 sf<px : supf0 s o< px
1075 sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sym sfpx=px)) ss<spx
1076 -- (sf1=sf0 ?) (trans ? sfpx=px ) ss<spx
1077 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
1078 csupf17 (init as refl ) = ZChain.csupf zc sf<px
1079 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
1080
1065 1081
1066 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where 1082 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
1067 field 1083 field
1068 tsup : MinSUP A (UnionCF A f mf ay supf1 z) 1084 tsup : MinSUP A (UnionCF A f mf ay supf1 z)
1069 tsup=sup : supf1 z ≡ MinSUP.sup tsup 1085 tsup=sup : supf1 z ≡ MinSUP.sup tsup
1078 m = ZChain.minsup zc (o≤-refl0 b) 1094 m = ZChain.minsup zc (o≤-refl0 b)
1079 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 1095 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
1080 ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } 1096 ; x<sup = ? ; minsup = ? } ; tsup=sup = ? }
1081 1097
1082 1098
1083 csupf1 : {b : Ordinal } → supf1 b o< x → odef (UnionCF A f mf ay supf1 x) (supf1 b) 1099 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
1084 csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf1 b) sb<z 1100 csupf1 {z1} sz1<x with trio< (supf0 z1) px
1085 record { fcy<sup = ? ; order = order ; supu=u = ? } 1101 ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) (sym (sf1=sf0 z1≤px)) (case1 (ZChain.csupf zc a )) where
1086 (init ? ? ) ⟫ where 1102 z1≤px : z1 o≤ px
1087 b<x : b o< x 1103 z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a ))
1088 b<x = ZChain.supf-inject zc ? 1104 ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where
1089 asb : odef A (supf1 b) 1105 z1≤px : z1 o≤ px
1090 asb = ? -- ZChain.supf∈A zc ? -- (o<→≤ b<x) 1106 z1≤px with trio< z1 px
1091 supb : SUP A (UnionCF A f mf ay supf1 (supf1 b)) 1107 ... | tri< a ¬b ¬c = o<→≤ a
1092 supb = ? -- ZChain.sup zc (o<→≤ sb<z) 1108 ... | tri≈ ¬a b ¬c = o≤-refl0 b
1093 supb-is-b : supf1 (supf1 b) ≡ & (SUP.sup supb) 1109 ... | tri> ¬a ¬b c = ⊥-elim ( o<> c ( supf-inject0 supf-mono1 (subst (λ k → supf1 z1 o< k ) refl ?) ) )
1094 supb-is-b = ? -- ZChain.supf-is-sup zc ? -- (o<→≤ sb<z) 1110 zc20 : supf0 px ≡ supf1 z1
1095 order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) → 1111 zc20 = begin
1096 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b)) 1112 supf0 px ≡⟨ ? ⟩
1097 order {s} {z1} ss<ssb fs with SUP.x<sup supb ? 1113 px ≡⟨ ? ⟩
1098 ... | case1 eq = ? 1114 supf0 z1 ≡⟨ ? ⟩
1099 ... | case2 lt = ? 1115 supf1 z1 ∎ where open ≡-Reasoning
1116 ... | tri> ¬a ¬b c = ⊥-elim ( ? )
1100 1117
1101 ... | case2 px<spfx = ? where 1118 ... | case2 px<spfx = ? where
1102 1119
1103 -- case2 : px o< supf px 1120 -- case2 : px o< supf px
1104 -- supf px is not MinSUP of previous chain , supf x ≡ supf px 1121 -- supf px is not MinSUP of previous chain , supf x ≡ supf px