src/HOL/UNITY/SubstAx.thy
changeset 13796 19f50fa807ae
parent 9685 6d123a7e30bd
child 13798 4c1a53627500
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Jan 29 17:35:11 2003 +0100
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Jan 30 10:35:56 2003 +0100
     1.3 @@ -6,16 +6,416 @@
     1.4  Weak LeadsTo relation (restricted to the set of reachable states)
     1.5  *)
     1.6  
     1.7 -SubstAx = WFair + Constrains + 
     1.8 +theory SubstAx = WFair + Constrains:
     1.9  
    1.10  constdefs
    1.11 -   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
    1.12 +   Ensures :: "['a set, 'a set] => 'a program set"    (infixl "Ensures" 60)
    1.13      "A Ensures B == {F. F : (reachable F Int A) ensures B}"
    1.14  
    1.15 -   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
    1.16 +   LeadsTo :: "['a set, 'a set] => 'a program set"    (infixl "LeadsTo" 60)
    1.17      "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
    1.18  
    1.19  syntax (xsymbols)
    1.20 -  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
    1.21 +  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
    1.22 +
    1.23 +
    1.24 +(*Resembles the previous definition of LeadsTo*)
    1.25 +lemma LeadsTo_eq_leadsTo: 
    1.26 +     "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"
    1.27 +apply (unfold LeadsTo_def)
    1.28 +apply (blast dest: psp_stable2 intro: leadsTo_weaken)
    1.29 +done
    1.30 +
    1.31 +
    1.32 +(*** Specialized laws for handling invariants ***)
    1.33 +
    1.34 +(** Conjoining an Always property **)
    1.35 +
    1.36 +lemma Always_LeadsTo_pre:
    1.37 +     "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')"
    1.38 +by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
    1.39 +
    1.40 +lemma Always_LeadsTo_post:
    1.41 +     "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')"
    1.42 +by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
    1.43 +
    1.44 +(* [| F : Always C;  F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
    1.45 +lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
    1.46 +
    1.47 +(* [| F : Always INV;  F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
    1.48 +lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
    1.49 +
    1.50 +
    1.51 +(*** Introduction rules: Basis, Trans, Union ***)
    1.52 +
    1.53 +lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
    1.54 +apply (simp add: LeadsTo_def)
    1.55 +apply (blast intro: leadsTo_weaken_L)
    1.56 +done
    1.57 +
    1.58 +lemma LeadsTo_Trans:
    1.59 +     "[| F : A LeadsTo B;  F : B LeadsTo C |] ==> F : A LeadsTo C"
    1.60 +apply (simp add: LeadsTo_eq_leadsTo)
    1.61 +apply (blast intro: leadsTo_Trans)
    1.62 +done
    1.63 +
    1.64 +lemma LeadsTo_Union: 
    1.65 +     "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B"
    1.66 +apply (simp add: LeadsTo_def)
    1.67 +apply (subst Int_Union)
    1.68 +apply (blast intro: leadsTo_UN)
    1.69 +done
    1.70 +
    1.71 +
    1.72 +(*** Derived rules ***)
    1.73 +
    1.74 +lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
    1.75 +by (simp add: LeadsTo_def)
    1.76 +
    1.77 +(*Useful with cancellation, disjunction*)
    1.78 +lemma LeadsTo_Un_duplicate:
    1.79 +     "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"
    1.80 +by (simp add: Un_ac)
    1.81 +
    1.82 +lemma LeadsTo_Un_duplicate2:
    1.83 +     "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)"
    1.84 +by (simp add: Un_ac)
    1.85 +
    1.86 +lemma LeadsTo_UN: 
    1.87 +     "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B"
    1.88 +apply (simp only: Union_image_eq [symmetric])
    1.89 +apply (blast intro: LeadsTo_Union)
    1.90 +done
    1.91 +
    1.92 +(*Binary union introduction rule*)
    1.93 +lemma LeadsTo_Un:
    1.94 +     "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"
    1.95 +apply (subst Un_eq_Union)
    1.96 +apply (blast intro: LeadsTo_Union)
    1.97 +done
    1.98 +
    1.99 +(*Lets us look at the starting state*)
   1.100 +lemma single_LeadsTo_I:
   1.101 +     "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B"
   1.102 +by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
   1.103 +
   1.104 +lemma subset_imp_LeadsTo: "A <= B ==> F : A LeadsTo B"
   1.105 +apply (simp add: LeadsTo_def)
   1.106 +apply (blast intro: subset_imp_leadsTo)
   1.107 +done
   1.108 +
   1.109 +lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
   1.110 +
   1.111 +lemma LeadsTo_weaken_R [rule_format]:
   1.112 +     "[| F : A LeadsTo A';  A' <= B' |] ==> F : A LeadsTo B'"
   1.113 +apply (simp (no_asm_use) add: LeadsTo_def)
   1.114 +apply (blast intro: leadsTo_weaken_R)
   1.115 +done
   1.116 +
   1.117 +lemma LeadsTo_weaken_L [rule_format]:
   1.118 +     "[| F : A LeadsTo A';  B <= A |]   
   1.119 +      ==> F : B LeadsTo A'"
   1.120 +apply (simp (no_asm_use) add: LeadsTo_def)
   1.121 +apply (blast intro: leadsTo_weaken_L)
   1.122 +done
   1.123 +
   1.124 +lemma LeadsTo_weaken:
   1.125 +     "[| F : A LeadsTo A';    
   1.126 +         B  <= A;   A' <= B' |]  
   1.127 +      ==> F : B LeadsTo B'"
   1.128 +by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
   1.129 +
   1.130 +lemma Always_LeadsTo_weaken:
   1.131 +     "[| F : Always C;  F : A LeadsTo A';    
   1.132 +         C Int B <= A;   C Int A' <= B' |]  
   1.133 +      ==> F : B LeadsTo B'"
   1.134 +by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD)
   1.135 +
   1.136 +(** Two theorems for "proof lattices" **)
   1.137 +
   1.138 +lemma LeadsTo_Un_post: "F : A LeadsTo B ==> F : (A Un B) LeadsTo B"
   1.139 +by (blast intro: LeadsTo_Un subset_imp_LeadsTo)
   1.140 +
   1.141 +lemma LeadsTo_Trans_Un:
   1.142 +     "[| F : A LeadsTo B;  F : B LeadsTo C |]  
   1.143 +      ==> F : (A Un B) LeadsTo C"
   1.144 +by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans)
   1.145 +
   1.146 +
   1.147 +(** Distributive laws **)
   1.148 +
   1.149 +lemma LeadsTo_Un_distrib:
   1.150 +     "(F : (A Un B) LeadsTo C)  = (F : A LeadsTo C & F : B LeadsTo C)"
   1.151 +by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
   1.152 +
   1.153 +lemma LeadsTo_UN_distrib:
   1.154 +     "(F : (UN i:I. A i) LeadsTo B)  =  (ALL i : I. F : (A i) LeadsTo B)"
   1.155 +by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
   1.156 +
   1.157 +lemma LeadsTo_Union_distrib:
   1.158 +     "(F : (Union S) LeadsTo B)  =  (ALL A : S. F : A LeadsTo B)"
   1.159 +by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
   1.160 +
   1.161 +
   1.162 +(** More rules using the premise "Always INV" **)
   1.163 +
   1.164 +lemma LeadsTo_Basis: "F : A Ensures B ==> F : A LeadsTo B"
   1.165 +by (simp add: Ensures_def LeadsTo_def leadsTo_Basis)
   1.166 +
   1.167 +lemma EnsuresI:
   1.168 +     "[| F : (A-B) Co (A Un B);  F : transient (A-B) |]    
   1.169 +      ==> F : A Ensures B"
   1.170 +apply (simp add: Ensures_def Constrains_eq_constrains)
   1.171 +apply (blast intro: ensuresI constrains_weaken transient_strengthen)
   1.172 +done
   1.173 +
   1.174 +lemma Always_LeadsTo_Basis:
   1.175 +     "[| F : Always INV;       
   1.176 +         F : (INV Int (A-A')) Co (A Un A');  
   1.177 +         F : transient (INV Int (A-A')) |]    
   1.178 +  ==> F : A LeadsTo A'"
   1.179 +apply (rule Always_LeadsToI, assumption)
   1.180 +apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
   1.181 +done
   1.182 +
   1.183 +(*Set difference: maybe combine with leadsTo_weaken_L??
   1.184 +  This is the most useful form of the "disjunction" rule*)
   1.185 +lemma LeadsTo_Diff:
   1.186 +     "[| F : (A-B) LeadsTo C;  F : (A Int B) LeadsTo C |]  
   1.187 +      ==> F : A LeadsTo C"
   1.188 +by (blast intro: LeadsTo_Un LeadsTo_weaken)
   1.189 +
   1.190 +
   1.191 +lemma LeadsTo_UN_UN: 
   1.192 +     "(!! i. i:I ==> F : (A i) LeadsTo (A' i))  
   1.193 +      ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)"
   1.194 +apply (simp only: Union_image_eq [symmetric])
   1.195 +apply (blast intro: LeadsTo_Union LeadsTo_weaken_R)
   1.196 +done
   1.197 +
   1.198 +
   1.199 +(*Version with no index set*)
   1.200 +lemma LeadsTo_UN_UN_noindex: 
   1.201 +     "(!! i. F : (A i) LeadsTo (A' i))  
   1.202 +      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
   1.203 +by (blast intro: LeadsTo_UN_UN)
   1.204 +
   1.205 +(*Version with no index set*)
   1.206 +lemma all_LeadsTo_UN_UN:
   1.207 +     "ALL i. F : (A i) LeadsTo (A' i)  
   1.208 +      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
   1.209 +by (blast intro: LeadsTo_UN_UN)
   1.210 +
   1.211 +(*Binary union version*)
   1.212 +lemma LeadsTo_Un_Un:
   1.213 +     "[| F : A LeadsTo A'; F : B LeadsTo B' |]  
   1.214 +            ==> F : (A Un B) LeadsTo (A' Un B')"
   1.215 +by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
   1.216 +
   1.217 +
   1.218 +(** The cancellation law **)
   1.219 +
   1.220 +lemma LeadsTo_cancel2:
   1.221 +     "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |]     
   1.222 +      ==> F : A LeadsTo (A' Un B')"
   1.223 +by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans)
   1.224 +
   1.225 +lemma LeadsTo_cancel_Diff2:
   1.226 +     "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |]  
   1.227 +      ==> F : A LeadsTo (A' Un B')"
   1.228 +apply (rule LeadsTo_cancel2)
   1.229 +prefer 2 apply assumption
   1.230 +apply (simp_all (no_asm_simp))
   1.231 +done
   1.232 +
   1.233 +lemma LeadsTo_cancel1:
   1.234 +     "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |]  
   1.235 +      ==> F : A LeadsTo (B' Un A')"
   1.236 +apply (simp add: Un_commute)
   1.237 +apply (blast intro!: LeadsTo_cancel2)
   1.238 +done
   1.239 +
   1.240 +lemma LeadsTo_cancel_Diff1:
   1.241 +     "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |]  
   1.242 +      ==> F : A LeadsTo (B' Un A')"
   1.243 +apply (rule LeadsTo_cancel1)
   1.244 +prefer 2 apply assumption
   1.245 +apply (simp_all (no_asm_simp))
   1.246 +done
   1.247 +
   1.248 +
   1.249 +(** The impossibility law **)
   1.250 +
   1.251 +(*The set "A" may be non-empty, but it contains no reachable states*)
   1.252 +lemma LeadsTo_empty: "F : A LeadsTo {} ==> F : Always (-A)"
   1.253 +apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
   1.254 +apply (drule leadsTo_empty, auto)
   1.255 +done
   1.256 +
   1.257 +
   1.258 +(** PSP: Progress-Safety-Progress **)
   1.259 +
   1.260 +(*Special case of PSP: Misra's "stable conjunction"*)
   1.261 +lemma PSP_Stable:
   1.262 +     "[| F : A LeadsTo A';  F : Stable B |]  
   1.263 +      ==> F : (A Int B) LeadsTo (A' Int B)"
   1.264 +apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Stable_eq_stable)
   1.265 +apply (drule psp_stable, assumption)
   1.266 +apply (simp add: Int_ac)
   1.267 +done
   1.268 +
   1.269 +lemma PSP_Stable2:
   1.270 +     "[| F : A LeadsTo A'; F : Stable B |]  
   1.271 +      ==> F : (B Int A) LeadsTo (B Int A')"
   1.272 +by (simp add: PSP_Stable Int_ac)
   1.273 +
   1.274 +lemma PSP:
   1.275 +     "[| F : A LeadsTo A'; F : B Co B' |]  
   1.276 +      ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
   1.277 +apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
   1.278 +apply (blast dest: psp intro: leadsTo_weaken)
   1.279 +done
   1.280 +
   1.281 +lemma PSP2:
   1.282 +     "[| F : A LeadsTo A'; F : B Co B' |]  
   1.283 +      ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"
   1.284 +by (simp add: PSP Int_ac)
   1.285 +
   1.286 +lemma PSP_Unless: 
   1.287 +     "[| F : A LeadsTo A'; F : B Unless B' |]  
   1.288 +      ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"
   1.289 +apply (unfold Unless_def)
   1.290 +apply (drule PSP, assumption)
   1.291 +apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
   1.292 +done
   1.293 +
   1.294 +
   1.295 +lemma Stable_transient_Always_LeadsTo:
   1.296 +     "[| F : Stable A;  F : transient C;   
   1.297 +         F : Always (-A Un B Un C) |] ==> F : A LeadsTo B"
   1.298 +apply (erule Always_LeadsTo_weaken)
   1.299 +apply (rule LeadsTo_Diff)
   1.300 +   prefer 2
   1.301 +   apply (erule
   1.302 +          transient_imp_leadsTo [THEN leadsTo_imp_LeadsTo, THEN PSP_Stable2])
   1.303 +   apply (blast intro: subset_imp_LeadsTo)+
   1.304 +done
   1.305 +
   1.306 +
   1.307 +(*** Induction rules ***)
   1.308 +
   1.309 +(** Meta or object quantifier ????? **)
   1.310 +lemma LeadsTo_wf_induct:
   1.311 +     "[| wf r;      
   1.312 +         ALL m. F : (A Int f-`{m}) LeadsTo                      
   1.313 +                            ((A Int f-`(r^-1 `` {m})) Un B) |]  
   1.314 +      ==> F : A LeadsTo B"
   1.315 +apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo)
   1.316 +apply (erule leadsTo_wf_induct)
   1.317 +apply (blast intro: leadsTo_weaken)
   1.318 +done
   1.319 +
   1.320 +
   1.321 +lemma Bounded_induct:
   1.322 +     "[| wf r;      
   1.323 +         ALL m:I. F : (A Int f-`{m}) LeadsTo                    
   1.324 +                              ((A Int f-`(r^-1 `` {m})) Un B) |]  
   1.325 +      ==> F : A LeadsTo ((A - (f-`I)) Un B)"
   1.326 +apply (erule LeadsTo_wf_induct, safe)
   1.327 +apply (case_tac "m:I")
   1.328 +apply (blast intro: LeadsTo_weaken)
   1.329 +apply (blast intro: subset_imp_LeadsTo)
   1.330 +done
   1.331 +
   1.332 +
   1.333 +lemma LessThan_induct:
   1.334 +     "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B))  
   1.335 +      ==> F : A LeadsTo B"
   1.336 +apply (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
   1.337 +done
   1.338 +
   1.339 +(*Integer version.  Could generalize from 0 to any lower bound*)
   1.340 +lemma integ_0_le_induct:
   1.341 +     "[| F : Always {s. (0::int) <= f s};   
   1.342 +         !! z. F : (A Int {s. f s = z}) LeadsTo                      
   1.343 +                            ((A Int {s. f s < z}) Un B) |]  
   1.344 +      ==> F : A LeadsTo B"
   1.345 +apply (rule_tac f = "nat o f" in LessThan_induct)
   1.346 +apply (simp add: vimage_def)
   1.347 +apply (rule Always_LeadsTo_weaken, assumption+)
   1.348 +apply (auto simp add: nat_eq_iff nat_less_iff)
   1.349 +done
   1.350 +
   1.351 +lemma LessThan_bounded_induct:
   1.352 +     "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo    
   1.353 +                                         ((A Int f-`(lessThan m)) Un B) |]  
   1.354 +            ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)"
   1.355 +apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
   1.356 +apply (rule wf_less_than [THEN Bounded_induct])
   1.357 +apply (simp (no_asm_simp))
   1.358 +done
   1.359 +
   1.360 +lemma GreaterThan_bounded_induct:
   1.361 +     "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo    
   1.362 +                               ((A Int f-`(greaterThan m)) Un B) |]  
   1.363 +      ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)"
   1.364 +apply (rule_tac f = f and f1 = "%k. l - k" 
   1.365 +       in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
   1.366 +apply (simp add: inv_image_def Image_singleton, clarify)
   1.367 +apply (case_tac "m<l")
   1.368 + prefer 2 apply (blast intro: not_leE subset_imp_LeadsTo)
   1.369 +apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
   1.370 +done
   1.371 +
   1.372 +
   1.373 +(*** Completion: Binary and General Finite versions ***)
   1.374 +
   1.375 +lemma Completion:
   1.376 +     "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C);  
   1.377 +         F : B LeadsTo (B' Un C);  F : B' Co (B' Un C) |]  
   1.378 +      ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"
   1.379 +apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
   1.380 +apply (blast intro: completion leadsTo_weaken)
   1.381 +done
   1.382 +
   1.383 +lemma Finite_completion_lemma:
   1.384 +     "finite I  
   1.385 +      ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->   
   1.386 +          (ALL i:I. F : (A' i) Co (A' i Un C)) -->  
   1.387 +          F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
   1.388 +apply (erule finite_induct, auto)
   1.389 +apply (rule Completion)
   1.390 +   prefer 4
   1.391 +   apply (simp only: INT_simps [symmetric])
   1.392 +   apply (rule Constrains_INT, auto)
   1.393 +done
   1.394 +
   1.395 +lemma Finite_completion: 
   1.396 +     "[| finite I;   
   1.397 +         !!i. i:I ==> F : (A i) LeadsTo (A' i Un C);  
   1.398 +         !!i. i:I ==> F : (A' i) Co (A' i Un C) |]    
   1.399 +      ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
   1.400 +by (blast intro: Finite_completion_lemma [THEN mp, THEN mp])
   1.401 +
   1.402 +lemma Stable_completion: 
   1.403 +     "[| F : A LeadsTo A';  F : Stable A';    
   1.404 +         F : B LeadsTo B';  F : Stable B' |]  
   1.405 +      ==> F : (A Int B) LeadsTo (A' Int B')"
   1.406 +apply (unfold Stable_def)
   1.407 +apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R])
   1.408 +apply (force+)
   1.409 +done
   1.410 +
   1.411 +lemma Finite_stable_completion: 
   1.412 +     "[| finite I;   
   1.413 +         !!i. i:I ==> F : (A i) LeadsTo (A' i);  
   1.414 +         !!i. i:I ==> F : Stable (A' i) |]    
   1.415 +      ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)"
   1.416 +apply (unfold Stable_def)
   1.417 +apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
   1.418 +apply (simp_all (no_asm_simp))
   1.419 +apply blast+
   1.420 +done
   1.421 +
   1.422  
   1.423  end