You are an expert at summarizing long articles. Proceed to summarize the following text: 
in 1985 , hoare s paper _ a couple of novelties in the propositional calculus _  @xcite was published . in this paper the ternary connective @xmath0 is introduced as the _ conditional_. with @xmath1 and @xmath2 denoting programs and @xmath3 a boolean expression . ] a more common expression for a conditional statement @xmath4 is @xmath5 but in order to reason systematically with conditional statements , a notation such as @xmath6 is preferable . in a conditional statement @xmath6 , first @xmath2 is evaluated , and depending on that evaluation result , then either @xmath1 or @xmath7 is evaluated ( and the other is not ) and determines the evaluation value . this evaluation strategy is a form of _ short - circuit _ evaluation . in @xcite , hoare proves that propositional logic is characterized by eleven equational axioms , some of which employ constants @xmath8 and @xmath9  for the truth values @xmath10  and @xmath11 .    in 2011 , we introduced _ proposition algebra _ in  @xcite as a general approach to the study of the conditional : we defined several _ valuation congruences _ and provided equational axiomatizations of these congruences . the most basic and least identifying valuation congruence is _ free _ valuation congruence , which is axiomatized by the axioms in table  [ cp ] .    ' '' ''    @xmath12    ' '' ''    [ cp ]    these axioms stem from  @xcite and define the conditional as a primitive connective . we use the name @xmath13  ( for conditional propositions ) for this set of axioms . interpreting a conditional statement as an if - then - else expression , axioms  @xmath14 are natural , and axiom   ( distributivity ) can be clarified by case analysis : if @xmath15 evaluates to @xmath10  and @xmath16 as well , then @xmath17 determines the result of evaluation ; if @xmath15 evaluates to @xmath10  and @xmath16 evaluates to @xmath11 , then @xmath18 determines the result of evaluation , and so on and so forth .    in section  [ sec : free ] we characterize free valuation congruence with help of _ evaluation trees _ : given a conditional statement , its evaluation tree directly represents all its evaluations ( in the way a truth table does in the case of propositional logic ) . two conditional statements are equivalent with respect to free valuation congruence if their evaluation trees are equal . evaluation trees are simple binary trees , proposed by daan staudt in  @xcite ( that appeared in 2012 ) . free valuation congruence identifies less than the equivalence defined by hoare s axioms in  @xcite . for example , the atomic proposition @xmath19 and the conditional statement @xmath20 are not equivalent with respect to free valuation congruence , although they are equivalent with respect to _ static _ valuation congruence , which is the valuation congruence that characterizes propositional logic . a valuation congruence that identifies more than free and less than static valuation congruence is _ repetition - proof _ valuation congruence , which has an axiomatization that comprises two more ( schematic ) axioms , one of which reads @xmath21 and thus expresses that if @xmath19 evaluates to @xmath11 , a consecutive evaluation of @xmath19 also evaluates to @xmath11 , so the conditional statement at the @xmath16-position will not be evaluated and can be replaced by any other . as an example , @xmath22 , and the left - hand and right - hand conditional statements are equivalent with respect to repetition - proof valuation congruence , but are not equivalent with respect to free valuation congruence .    in section  [ sec : rp ] we characterize repetition - proof valuation congruence by defining a transformation on evaluation trees that yields _ repetition - proof _ evaluation trees : two conditional statements are equivalent with respect to repetition - proof valuation congruence if , and only if , they have equal repetition - proof evaluation trees . although this transformation on evaluation trees is simple and natural , our proof of the mentioned characterization |which is phrased as a completeness result| is non - trivial and we could not find a proof that is essentially simpler . valuation congruences that identify more conditional statements than repetition - proof valuation congruence are contractive , memorizing , and static valuation congruence , and these are all defined and axiomatized in  @xcite . in sections @xmath23 , each of these valuation congruences is characterized using a transformation on evaluation trees : two conditional statements are c - valuation congruent if , and only if , their c - transformed evaluation trees are equal . these transformations are simple and natural , and only for static valuation congruence we use a slightly more complex transformation . in section [ sec : conc ] we discuss the general structure of the proofs of these results , which are all based on normalization of conditional statements . the paper ends with a brief digression on short - circuit logic , an example on the use of repetition - proof valuation congruence , and some remarks about side effects . a spin - off of our approach can be called `` basic form semantics for proposition algebra '' : for each valuation congruence c that we consider ( including the case c = free ) , two conditional statements are c - valuation congruent if , and only if , they have equal c - basic forms , where c - basic forms are obtained by a syntactic transformation of conditional statements , which is a form of normalization . consider the signature @xmath24 with constants @xmath25  and @xmath9for the truth values @xmath10  and @xmath11 , respectively , and constants @xmath19 for atomic propositions , further called _ atoms _ , from some countable set @xmath26 . we write @xmath27 for the set of closed terms , or _ conditional statements _ , over the signature @xmath28 . given a conditional statement @xmath6 , we refer to @xmath2 as its _ central condition_.    we define the _ dual _ @xmath29 of @xmath30 as follows : @xmath31 observe that @xmath13  is a self - dual axiomatization : when defining @xmath32 for each variable @xmath17 , the dual of each axiom is also in @xmath13 , and hence @xmath33    a natural view on conditional statements in @xmath34involves short - circuit evaluation , similar to how we consider the evaluation of an `` @xmath35 '' expression . the following definition is taken from  @xcite . [ def : trees ] the set @xmath36  of * evaluation trees over @xmath26 with leaves in @xmath37 * is defined inductively by @xmath38 the operator @xmath39 is called * post - conditional composition over @xmath19*. in the evaluation tree @xmath40 , the root is represented by @xmath19 , the left branch by @xmath41 and the right branch by @xmath42 .    we refer to trees in @xmath36  as evaluation trees , or trees for short . post - conditional composition and its notation stem from  @xcite . evaluation trees play a crucial role in the main results of  @xcite . in order to define our `` evaluation tree semantics '' , we first define the _ leaf replacement _ operator , ` replacement ' for short , on trees in @xmath36  as follows . let @xmath43 and @xmath44 . the replacement of @xmath25  with @xmath42 and @xmath45 with @xmath46 in @xmath41 , denoted @xmath47,\ ] ] is defined by @xmath48&= y,\\ { \ensuremath{{\sf f}}}[{\ensuremath{{\sf t}}}\mapsto y,{\ensuremath{{\sf f}}}\mapsto z]&= z,\\ ( x'{{\raisebox{1pt}{\footnotesize$\;\underline{\triangleleft}~$}}}a{{\raisebox{1pt}{\footnotesize$~\underline{\triangleright}\;$}}}x'')[{\ensuremath{{\sf t}}}\mapsto y,{\ensuremath{{\sf f}}}\mapsto z ] & = x'[{\ensuremath{{\sf t}}}\mapsto y,{\ensuremath{{\sf f}}}\mapsto z]{{\raisebox{1pt}{\footnotesize$\;\underline{\triangleleft}~$}}}a{{\raisebox{1pt}{\footnotesize$~\underline{\triangleright}\;$}}}x''[{\ensuremath{{\sf t}}}\mapsto y,{\ensuremath{{\sf f}}}\mapsto z].\end{aligned}\ ] ] we note that the order in which the replacements of leaves of @xmath41 is listed is irrelevant and we adopt the convention of not listing identities inside the brackets , e.g. , @xmath49=x[{\ensuremath{{\sf t}}}\mapsto { \ensuremath{{\sf t}}},{\ensuremath{{\sf f}}}\mapsto z]$ ] . furthermore , repeated replacements satisfy the following equation : @xmath50\big)\;[{\ensuremath{{\sf t}}}\mapsto y_2,{\ensuremath{{\sf f}}}\mapsto z_2]\\ & = x[{\ensuremath{{\sf t}}}\mapsto y_1[{\ensuremath{{\sf t}}}\mapsto y_2,{\ensuremath{{\sf f}}}\mapsto z_2],~ { \ensuremath{{\sf f}}}\mapsto z_1[{\ensuremath{{\sf t}}}\mapsto y_2,{\ensuremath{{\sf f}}}\mapsto z_2]].\end{aligned}\ ] ]    we now have the terminology and notation to define the interpretation of conditional statements in @xmath34  as evaluation trees by a function @xmath51 ( abbreviating short - circuit evaluation ) . [ def : se ] the * short - circuit evaluation function * @xmath52 is defined as follows , where @xmath53 : @xmath54.\end{aligned}\ ] ]    [ ex : fr ] the conditional statement @xmath55 yields the following evaluation tree : @xmath56\\ & = ( { \ensuremath{{\sf f}}}{{\raisebox{1pt}{\footnotesize$\;\underline{\triangleleft}~$}}}a{{\raisebox{1pt}{\footnotesize$~\underline{\triangleright}\;$}}}{\ensuremath{{\sf t}}})[{\ensuremath{{\sf t}}}\mapsto se(a)]\\ & = { \ensuremath{{\sf f}}}{{\raisebox{1pt}{\footnotesize$\;\underline{\triangleleft}~$}}}a{{\raisebox{1pt}{\footnotesize$~\underline{\triangleright}\;$}}}({\ensuremath{{\sf t}}}{{\raisebox{1pt}{\footnotesize$\;\underline{\triangleleft}~$}}}a{{\raisebox{1pt}{\footnotesize$~\underline{\triangleright}\;$}}}{\ensuremath{{\sf f}}}).\end{aligned}\ ] ] a more pictorial representation of this evaluation tree is the following , where @xmath57 yields a left branch and @xmath58 a right branch : @xmath59        \node ( a ) { $ a$ }          child { node ( b1 ) { $ { \ensuremath{{\sf f}}}$ }          }          child { node ( b2 ) { $ a$ }            child { node ( d1 ) { $ { \ensuremath{{\sf t}}}$ } }             child { node ( d2 ) { $ { \ensuremath{{\sf f}}}$ } }          } ; \end{tikzpicture}\ ] ] _ end example . _    as we can see from the definition on atoms , evaluation continues in the left branch if an atom evaluates to @xmath10  and in the right branch if it evaluates to @xmath11 . we shall often use the constants @xmath25  and @xmath9  to denote the result of an evaluation ( instead of @xmath10  and @xmath11 ) . [ def : eval ] let @xmath30 . an * evaluation * of @xmath1 is a pair @xmath60 where @xmath61 and @xmath62 , such that if @xmath63 , then @xmath64 ( the empty string ) and @xmath65 , and otherwise , @xmath66 where @xmath67 is a complete path in @xmath68 and    * for @xmath69 , if @xmath70 is a left child of @xmath71 then @xmath72 , and otherwise @xmath73 , * if @xmath74 is a left child of @xmath75 then @xmath76 , and otherwise @xmath77 . we refer to @xmath78 as the * evaluation path * and to @xmath74 as the * evaluation result*.    so , an evaluation of a conditional statement @xmath1 is a complete path in @xmath68 ( from root to leaf ) and contains evaluation values for all occurring atoms . for instance , the evaluation tree @xmath79 from example  [ ex : fr ] encodes the evaluations @xmath80 , @xmath81 , and @xmath82 . as an aside , we note that this particular evaluation tree encodes all possible evaluations of @xmath83 , where ` & & ` is the connective that prescribes _ short - circuit conjunction _ ( we return to this connective in section  [ sec : conc ] ) .    in turn , each evaluation tree gives rise to a _ unique _ conditional statement . for example  [ ex : fr ] , this is @xmath84 ( note the syntactical correspondence ) . [ def : basic ] * basic forms over @xmath26 * are defined by the following grammar @xmath85 we write @xmath86 for the set of basic forms over @xmath26 . the * depth * @xmath87 of @xmath88 is defined by @xmath89 and @xmath90 . the following lemma s exploit the structure of basic forms and are stepping stones to our first completeness result ( theorem  [ thm:1 ] ) . [ la:2.5 ] for each @xmath30 there exists @xmath91 such that @xmath92 . first we establish an auxiliary result : if @xmath93 are basic forms , then there is a basic form @xmath94 such that @xmath95 . this follows by structural induction on @xmath2 . the lemma s statement follows by structural induction on @xmath1 . the base cases @xmath96 are trivial , and if @xmath97 there exist by induction basic forms @xmath98 such that @xmath99 , hence @xmath100 . now apply the auxiliary result . [ la:2.6 ] for all basic forms @xmath1 and @xmath2 , @xmath101 implies @xmath102 .    by structural induction on @xmath1 the base cases @xmath103 are trivial . if @xmath104 , then @xmath105 and @xmath106 with @xmath107 , so @xmath108 and @xmath109 . by induction we find @xmath110 , and hence @xmath102 . [ def : freevc ] * free valuation congruence * , notation @xmath111 , is defined on @xmath34  as follows : @xmath112    [ la : x ] free valuation congruence is a congruence relation . let @xmath113 and assume @xmath114 , thus @xmath115 . then @xmath116= se(q)[{\ensuremath{{\sf t}}}\mapsto se(p'),{\ensuremath{{\sf f}}}\mapsto se(r)]=se(p'{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}q{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}r)$ ] , and thus @xmath117 . the two remaining cases can be proved in a similar way . [ thm:1 ] for all @xmath118 , @xmath119    we first prove @xmath120 . by lemma  [ la : x ] , @xmath111 is a congruence relation and it easily follows that all @xmath13-axioms are sound . for example , soundness of axiom   follows from @xmath121\\ & = \big(se(r)[{\ensuremath{{\sf t}}}\mapsto se(q),{\ensuremath{{\sf f}}}\mapsto se(s)]\big)\;[{\ensuremath{{\sf t}}}\mapsto se(p),{\ensuremath{{\sf f}}}\mapsto se(u)]\\ & = se(r)[{\ensuremath{{\sf t}}}\mapsto se(q)[{\ensuremath{{\sf t}}}\mapsto se(p),{\ensuremath{{\sf f}}}\mapsto se(u ) ] , { \ensuremath{{\sf f}}}\mapsto \,se(s)[{\ensuremath{{\sf t}}}\mapsto se(p),{\ensuremath{{\sf f}}}\mapsto se(u)]]\\ & = se(r)[{\ensuremath{{\sf t}}}\mapsto se(p{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}q{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}u),{\ensuremath{{\sf f}}}\mapsto se(p{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}s{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}u)]\\ & = se((p{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}q{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}u){{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}r{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}(p{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}s{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}u)).\end{aligned}\ ] ]    in order to prove @xmath122 , let @xmath123 . according to lemma  [ la:2.5 ] there exist basic forms @xmath124 and @xmath125 such that @xmath126 and @xmath127 , so @xmath128 . by soundness ( @xmath120 ) we find @xmath129 , so by lemma  [ la:2.6 ] , @xmath130 . hence , @xmath131 . a consequence of the above results is that for each @xmath30 there is a _ unique _ basic form @xmath124 with @xmath126 , and that for each basic form , its @xmath51-image has exactly the same syntactic structure ( replacing @xmath132 by @xmath57 , and @xmath133 by @xmath58 ) . in the remainder of this section , we make this precise . [ def : bf ] the * basic form function * @xmath134 is defined as follows , where @xmath53 : @xmath135.\end{aligned}\ ] ] given @xmath136 , the auxiliary function @xmath137:{\ensuremath{\textit{bf}_a}}\to{\ensuremath{\textit{bf}_a}}$ ] for which post - fix notation @xmath138 $ ] is adopted , is defined as follows : @xmath139&=q,\\ { \ensuremath{{\sf f}}}[{\ensuremath{{\sf t}}}\mapsto q , { \ensuremath{{\sf f}}}\mapsto r]&=r,\\ ( p_1{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}p_2)[{\ensuremath{{\sf t}}}\mapsto q , { \ensuremath{{\sf f}}}\mapsto r ] & = p_1[{\ensuremath{{\sf t}}}\mapsto q , { \ensuremath{{\sf f}}}\mapsto r]{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}p_2[{\ensuremath{{\sf t}}}\mapsto q , { \ensuremath{{\sf f}}}\mapsto r].\end{aligned}\ ] ] ( the notational overloading with the leaf replacement functions on valuation trees is harmless ) . so , for given @xmath140 , the auxiliary function @xmath141 $ ] applied to @xmath88 ( thus , @xmath142 $ ] ) replaces all @xmath25-occurrences in @xmath1 by @xmath2 , and all @xmath9-occurrences in @xmath1 by @xmath7 . the following two lemma s imply that @xmath143 is a normalization function . [ la : bf ] for all @xmath30 , @xmath144 is a basic form .    by structural induction . the base cases are trivial . for the inductive case we find @xmath145 $ ] , so by induction , @xmath144 , @xmath146 , and @xmath147 are basic forms . furthermore , replacing all @xmath25-occurrences and @xmath9-occurrences in @xmath146 by basic forms @xmath144 and @xmath147 , respectively , yields a basic form . [ la:2.12 ] for each basic form @xmath1 , @xmath148 .    by structural induction on @xmath1 . [ def : freevca ] the binary relation @xmath149 on @xmath34is defined as follows : @xmath150    [ la : rephrase ] the relation @xmath149 is a congruence relation .    let @xmath113 and assume @xmath151 , thus @xmath152 . then @xmath153= { \ensuremath{\mathit{bf}}}(q)[{\ensuremath{{\sf t}}}\mapsto { \ensuremath{\mathit{bf}}}(p'),{\ensuremath{{\sf f}}}\mapsto { \ensuremath{\mathit{bf}}}(r)]={\ensuremath{\mathit{bf}}}(p'{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}q{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}r)$ ] , and thus @xmath154 . the two remaining cases can be proved in a similar way .    before proving that @xmath13  is an axiomatization of the relation @xmath149 , we show that each instance of the axiom   satisfies @xmath149 . [ la : nieuw ] for all @xmath155 , @xmath156    by definition , the lemma s statement is equivalent with @xmath157\big)\;[{\ensuremath{{\sf t}}}\mapsto{\ensuremath{\mathit{bf}}}(q_1),{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(q_2)]\\ \label{eq : bf } & = { \ensuremath{\mathit{bf}}}(p)[{\ensuremath{{\sf t}}}\mapsto{\ensuremath{\mathit{bf}}}(q_1{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}p_1{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}q_2),{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(q_1{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}p_2{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}q_2)].\end{aligned}\ ] ] by lemma  [ la : bf ] , @xmath144 , @xmath158,and @xmath159 are basic forms . we prove   by structural induction on the form that @xmath144 can have . if @xmath160 , then @xmath161\big)&\;[{\ensuremath{{\sf t}}}\mapsto{\ensuremath{\mathit{bf}}}(q_1),{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(q_2 ) ] { \ensuremath{\mathit{bf}}}(p_1)[{\ensuremath{{\sf t}}}\mapsto{\ensuremath{\mathit{bf}}}(q_1),{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(q_2 ) ] \end{aligned}\ ] ] and @xmath162 & = { \ensuremath{\mathit{bf}}}(q_1{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}p_1{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}q_2)\\ & = { \ensuremath{\mathit{bf}}}(p_1)[{\ensuremath{{\sf t}}}\mapsto{\ensuremath{\mathit{bf}}}(q_1),{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(q_2)].\end{aligned}\ ] ] if @xmath163 , then   follows in a similar way . the inductive case @xmath164 is trivial ( by definition of the last defining clause of the auxiliary functions @xmath141 $ ] in definition  [ def : bf ] ) . [ thm:1a ] for all @xmath118 , @xmath165    we first prove @xmath120 . by lemma  [ la : rephrase ] , @xmath149 is a congruence relation and it easily follows that arbitrary instances of the @xmath13-axioms @xmath14 satisfy @xmath149 . by lemma  [ la : nieuw ] it follows that arbitrary instances of axiom   also satisfy @xmath149 .    in order to prove @xmath122 , assume @xmath166 . according to lemma  [ la:2.5 ] , there exist basic forms @xmath124 and @xmath125 such that @xmath126 and @xmath127 , so @xmath128 . by @xmath120 it follows that @xmath167 , which implies by lemma  [ la:2.12 ] that @xmath130 . hence , @xmath131 . [ cor:1 ] for all @xmath30 ,   @xmath168  and   @xmath169 .    by lemma [ la : bf ] and lemma  [ la:2.12 ] , @xmath170 , thus @xmath168 . by theorem  [ thm:1a ] , @xmath171 , and by theorem  [ thm:1 ] , @xmath169 . in  @xcite we defined _ repetition - proof _ @xmath13  as the extension of the axiom set @xmath13  with the following two axiom schemes , where @xmath19 ranges over @xmath26 : @xmath172 we write @xmath173 for this extension . these axiom schemes characterize that for each atom @xmath19 , a consecutive evaluation of @xmath19 yields the same result , so in both cases the conditional statement at the @xmath16-position will not be evaluated and can be replaced by any other . note that   and are each others dual . we define a proper subset of basic forms with the property that each propositional statement can be proved equal to such a basic form . [ def:3.1 ] * rp - basic forms * are inductively defined :    * @xmath25  and @xmath9  are rp - basic forms , and * @xmath174 is an rp - basic form if @xmath175 and @xmath176 are rp - basic forms , and if @xmath177 is not equal to @xmath25  or @xmath9 , then either the central condition in @xmath177 is different from @xmath19 , or @xmath177 is of the form @xmath178 .    it will turn out useful to define a function that transforms conditional statements into rp - basic forms , and that is comparable to the function @xmath143 . [ def:3.2 ] the * rp - basic form function * @xmath179 is defined by @xmath180 the auxiliary function @xmath181 is defined as follows : @xmath182 for @xmath53 , the auxiliary functions @xmath183 and @xmath184 are defined by @xmath185 and @xmath186    thus , @xmath187 maps a conditional statement @xmath1 to @xmath144 and then transforms @xmath144 according to the auxiliary functions @xmath188 , @xmath189 , and @xmath190 . [ la:3.3 ] for all @xmath53 and @xmath88 , @xmath191 and @xmath192 .    by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath193 we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath195 and @xmath196 follows in a similar way . if @xmath107 , then @xmath197 , and hence @xmath191 the second pair of equalities can be derived in a similar way .    in order to prove that for all @xmath30 , @xmath198 is an rp - basic form , we use the following auxiliary lemma . [ la:3.4 ] for all @xmath53 and @xmath88 , @xmath199 and @xmath200 . fix some @xmath53 . we prove these inequalities by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath193 we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath201 and @xmath202 follows in a similar way .    if @xmath107 , then @xmath197 , and hence @xmath199 and @xmath200 . [ la:3.5 ] for all @xmath30 , @xmath198 is an rp - basic form . we first prove an auxiliary result : @xmath203 this follows by induction on the depth @xmath87 of @xmath1 . if @xmath204 , then @xmath103 , and hence @xmath205 is an rp - basic form . for the inductive case @xmath206 it must be the case that @xmath207 . we find @xmath208 which is an rp - basic form because    * by lemma  [ la:3.4 ] , @xmath209 and @xmath210 are basic forms with depth smaller than or equal to @xmath211 , so by the induction hypothesis , @xmath212 and @xmath213 are rp - basic forms , * @xmath212 and @xmath213 both satisfy the following property : if the central condition ( if present ) is @xmath19 , then the outer arguments are equal . we show this first for @xmath212 by a case distinction on the form of @xmath2 : 1 .   if @xmath214 , then @xmath215 , so there is nothing to prove . 2 .   if @xmath216 , then @xmath217 and thus by lemma  [ la:3.3 ] , + @xmath218 . 3 .   if @xmath219 with @xmath107 , then @xmath220 , so + @xmath221 and there is nothing to prove . + the fact that @xmath213 satisfies this property follows in a similar way . this finishes the proof of  . the lemma s statement now follows by structural induction : the base cases ( comprising a single atom @xmath19 ) are again trivial , and for the inductive case , @xmath222 for some basic form @xmath94 by lemma  [ la : bf ] , and by auxiliary result  , @xmath223 is an rp - basic form . the following , rather technical result is used in proposition  [ prop:3.7 ] and lemma  [ la:3.8 ] . [ la:3.6 ] if @xmath224 is an rp - basic form , then @xmath225 and @xmath226 . we first prove an auxiliary result : @xmath227 we prove both equalities by simultaneous induction on the structure of @xmath2 and @xmath7 . the base case , thus @xmath228 , is trivial . if @xmath229 and @xmath230 , then @xmath2 and @xmath7 are rp - basic forms with central condition @xmath19 , so @xmath231 and the equality for @xmath7 follows in a similar way . if @xmath229 and @xmath232 , then @xmath233 , and the result follows as above . all remaining cases follow in a similar way , which finishes the proof of  . we now prove the lemma s statement by simultaneous induction on the structure of @xmath2 and @xmath7 . the base case , thus @xmath228 , is again trivial . if @xmath229 and @xmath230 , then by auxiliary result  , @xmath234 and by induction , @xmath235 . hence , @xmath236 , and @xmath237 and the equalities for @xmath7 follow in a similar way .    if @xmath229 and @xmath232 , the lemma s equalities follow in a similar way , although a bit simpler because @xmath238 .    for all remaining cases , the lemma s equalities follow in a similar way . [ prop:3.7 ] for all @xmath30 , @xmath198 is an rp - basic form , and for each rp - basic form @xmath1 , @xmath239 . the first statement is lemma  [ la:3.5 ] . for the second statement , it suffices by lemma  [ la:2.12 ] to prove that for each rp - basic form @xmath1 , @xmath205 . this follows by case distinction on @xmath1 . the cases @xmath103 follow immediately , and otherwise @xmath104 , and thus @xmath240 . by lemma  [ la:3.6 ] , @xmath241 and @xmath242 , hence @xmath205 . [ la:3.8 ] for all @xmath88 , @xmath243 . we apply structural induction on @xmath1 . the base cases @xmath103 are trivial . assume @xmath104 . by induction @xmath244 . we proceed by a case distinction on the form that @xmath175 and @xmath176 can have :    1 . if @xmath245 with @xmath246 , then @xmath247 and @xmath248 , and hence @xmath249 , and thus @xmath243 . 2 .   if @xmath250 and @xmath251 with @xmath107 , then @xmath248 and by auxiliary result   in the proof of lemma  [ la:3.5 ] , @xmath252 and @xmath253 are rp - basic forms . we derive @xmath254 3 . if @xmath255 with @xmath107 and @xmath256 , we can proceed as in the previous case , but now using axiom scheme   and the identity @xmath247 , and the fact that @xmath257 and @xmath258 are rp - basic forms . if @xmath250 and @xmath256 , we can proceed as in two previous cases , now using both   and , and the fact that @xmath252 and @xmath258 are rp - basic forms . +    [ thm:3.9 ] for all @xmath30 , @xmath259 .    by theorem  [ thm:1a ] and corollary  [ cor:1 ] we find @xmath260 . by lemma  [ la:3.8 ] , @xmath261 , and @xmath262 . [ def:3.10 ] the binary relation @xmath263 on @xmath34is defined as follows : @xmath264    [ thm:3.11 ] for all @xmath118 , @xmath265 . assume @xmath266 . by theorem  [ thm:3.9 ] , @xmath267 . in  @xcite the following two statements are proved ( theorem 6.3 and an auxiliary result in its proof ) , where @xmath268 is a binary relation on @xmath269 :    1 .   for all @xmath118,@xmath270 . 2 .   for all rp - basic forms @xmath1 and @xmath271 .    by lemma  [ la:3.5 ] these statements imply @xmath272 , that is , @xmath273 . assume @xmath273 . by lemma  [ la:2.12 ] , @xmath274 . by theorem  [ thm:1a ] , @xmath275 . by theorem  [ thm:3.9 ] , @xmath266 . so , the relation @xmath263 is axiomatized by @xmath173 , and is thus a congruence . with this observation in mind , we define a transformation on evaluation trees that mimics the function @xmath187 , and prove that equality of two such transformed trees characterizes the congruence that is axiomatized by @xmath173 . [ def:3.12 ] the unary * repetition - proof evaluation function * @xmath276 yields * repetition - proof evaluation trees * and is defined by @xmath277 the auxiliary function @xmath278 is defined as follows ( @xmath53 ) : @xmath279 for @xmath53 , the auxiliary functions @xmath280 and @xmath281 are defined by @xmath282 and @xmath283    [ ex : rp ] let @xmath284 . we depict @xmath68 ( as in example  [ ex : fr ] ) and the repetition - proof evaluation tree @xmath285 : @xmath286{ll } \begin{array}[t]{l } \\[-4 mm ] \begin{tikzpicture } [       level distance=7.5 mm ,        level 1/.style={sibling distance=30 mm } ,        level 2/.style={sibling distance=15 mm } ,        baseline=(current bounding box.center ) ]        \node ( a ) { $ a$ }          child { node ( b1 ) { $ { \ensuremath{{\sf f}}}$ }          }          child { node ( b2 ) { $ a$ }            child { node ( d1 ) { $ { \ensuremath{{\sf t}}}$ } }             child { node ( d2 ) { $ { \ensuremath{{\sf f}}}$ } }          } ; \end{tikzpicture } \end{array } & \qquad \begin{array}[t]{l } \\[-4 mm ] \qquad \begin{tikzpicture } [       level distance=7.5 mm ,        level 1/.style={sibling distance=30 mm } ,        level 2/.style={sibling distance=15 mm } ,        baseline=(current bounding box.center ) ]        \node ( a ) { $ a$ }          child { node ( b1 ) { $ { \ensuremath{{\sf f}}}$ }          }          child { node ( b2 ) { $ a$ }            child { node ( d1 ) { $ { \ensuremath{{\sf f}}}$ } }             child { node ( d2 ) { $ { \ensuremath{{\sf f}}}$ } }          } ; \end{tikzpicture } \\[-1 mm ] \end{array}\end{array}\ ] ] _ end example . _    the similarities between @xmath287 and the function @xmath187 can be exploited :    [ la:3.13 ] for all @xmath53 and @xmath288 , @xmath289 and + @xmath290 .    by structural induction on @xmath41 ( cf . the proof of lemma  [ la:3.3 ] ) . we use the following lemma in the proof of this section s last completeness result . [ la:3.14 ] for all @xmath88 , @xmath291 . we first prove an auxiliary result : @xmath292 we prove the first equality of by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath207 , let @xmath293 . we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath294 if @xmath107 , then @xmath295    the second equality can be proved in a similar way , and this finishes the proof of  . the lemma s statement now follows by a case distinction on @xmath1 . the cases @xmath103 follow immediately , and otherwise @xmath207 , and thus @xmath296    finally , we relate conditional statements by means of their repetition - proof evaluation trees . * repetition - proof valuation congruence * , notation @xmath297 , is defined on @xmath34  as follows : @xmath298    the following characterization result immediately implies that @xmath297 is a congruence relation on @xmath269 ( and hence justifies calling it a congruence ) . [ prop:3.16 ] for all @xmath118 , @xmath299 .    in order to prove @xmath120 , assume @xmath300 , thus @xmath301 . by corollary  [ cor:1 ] , @xmath302 , so by lemma  [ la:3.14 ] , @xmath303 . by lemma  [ la:2.6 ] and auxiliary result ( see the proof of lemma  [ la:3.5 ] ) , it follows that @xmath304 , that is , @xmath273 .    in order to prove @xmath122 , assume @xmath273 , thus @xmath304 and @xmath303 . by lemma  [ la:3.14 ] , @xmath302 . by corollary  [ cor:1 ] , @xmath305 and @xmath306 , so @xmath301 , that is , @xmath307 . we end this section with the completeness result we were after . [ thm:3.17 ] for all @xmath118 , @xmath308    combine theorem  [ thm:3.11 ] and proposition  [ prop:3.16 ] . in  @xcite we introduced @xmath309 , _ contractive _ @xmath13 , as the extension of @xmath13  with the following two axiom schemes , where @xmath19 ranges over @xmath26 : @xmath310 these schemes prescribe contraction for each atom @xmath19 for respectively the _ true_-case and the _ false_-case ( and are each others dual ) . it easily follows that the axiom schemes   and   are derivable from @xmath309 , so @xmath309 is also an axiomatic extension of @xmath173 . again , we define a proper subset of basic forms with the property that each propositional statement can be proved equal to such a basic form . [ def:4.1 ] * cr - basic forms * are inductively defined :    * @xmath25  and @xmath9  are cr - basic forms , and * @xmath174 is a cr - basic form if @xmath175 and @xmath176 are cr - basic forms , and if @xmath177 is not equal to @xmath25  or @xmath9 , the central condition in @xmath177 is different from @xmath19 .    it will turn out useful to define a function that transforms conditional statements into cr - basic forms , and that is comparable to the function @xmath143 ( see definition  [ def : bf ] ) . [ def:4.2 ] the * cr - basic form function * @xmath311 is defined by @xmath312 the auxiliary function @xmath313 is defined as follows : @xmath314 for @xmath53 , the auxiliary functions @xmath315 and @xmath316 are defined by @xmath317 and @xmath318    thus , @xmath319 maps a conditional statement @xmath1 to @xmath144 and then transforms @xmath144 according to the auxiliary functions @xmath320 , @xmath321 , and @xmath322 . [ la:4.3 ] for all @xmath53 and @xmath88 , @xmath323 and @xmath324 . fix some @xmath53 . we prove these inequalities by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath193 we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath325 and @xmath326 follows in a similar way .    if @xmath107 , then @xmath327 , and hence @xmath323 and @xmath324 . [ la:4.4 ] for all @xmath30 , @xmath328 is a cr - basic form . we first prove an auxiliary result : @xmath329 this follows by induction on the depth @xmath87 of @xmath1 . if @xmath204 , then @xmath103 , and hence @xmath330 is a cr - basic form . for the inductive case @xmath206 it must be the case that @xmath207 . we find @xmath331 which is a cr - basic form because    * by lemma  [ la:4.3 ] , @xmath332 and @xmath333 are basic forms with depth smaller than or equal to @xmath211 , so by the induction hypothesis , @xmath334 and @xmath335 are cr - basic forms , * by definition of the auxiliary functions @xmath321 and @xmath322 , the central condition of @xmath332 and @xmath333 is not equal to @xmath19 , hence @xmath336 is a cr - basic form . this completes the proof of  . the lemma s statement now follows by structural induction : the base cases ( comprising a single atom @xmath19 ) are again trivial , and for the inductive case , @xmath337 for some basic form @xmath94 by lemma  [ la : bf ] , and by  , @xmath338 is a cr - basic form .    the following , somewhat technical lemma is used in proposition  [ prop:4.6 ] and lemma  [ la:4.7 ] . [ la:4.5 ] if @xmath224 is a cr - basic form , then @xmath339 and @xmath340 .    by simultaneous induction on the structure of @xmath2 and @xmath7 . the base case , thus @xmath228 , is again trivial . if @xmath341 and @xmath342 , then @xmath343 and thus @xmath344 and @xmath345 . moreover , @xmath346 and @xmath347 have no central condition @xmath3 , hence @xmath348 and @xmath349 , and thus @xmath350 the equalities for @xmath7 follow in a similar way .    if @xmath351 and @xmath352 , the lemma s equalities follow in a similar way , and this is also the case if @xmath214 and @xmath353 .    with lemma  [ la:4.5 ] we can easily prove the following result . [ prop:4.6 ] for each @xmath30 , @xmath328 is a cr - basic form , and for each cr - basic form @xmath1 , @xmath354 . the first statement is lemma  [ la:4.4 ] . for the second statement , it suffices by lemma  [ la:2.12 ] to prove that @xmath330 . we prove this by case distinction on @xmath1 . the cases @xmath103 follow immediately , and otherwise @xmath104 , and thus @xmath355 . by lemma  [ la:4.5 ] , @xmath356 and @xmath357 , hence @xmath330 . [ la:4.7 ] for all @xmath88 , @xmath358 . we apply structural induction on @xmath1 . the base cases @xmath103 are trivial . assume @xmath104 . by induction @xmath359 . furthermore , by auxiliary result   in the proof of lemma  [ la:4.4 ] , @xmath360 is a cr - basic form , and by lemma  [ la:4.5 ] , @xmath361 we derive @xmath362    [ thm:4.8 ] for all @xmath30 , @xmath363 .    by theorem  [ thm:1a ] and corollary  [ cor:1 ] , @xmath364 , and by lemma  [ la:4.7 ] , @xmath365 , and @xmath366 . [ def:4.9 ] the binary relation @xmath367 on @xmath34is defined as follows : @xmath368    [ thm:4.10 ] for all @xmath118 , @xmath369 . assume @xmath370 . then , by theorem  [ thm:4.8 ] , @xmath371 . in  @xcite the following two statements are proved ( theorem 6.4 and an auxiliary result in its proof ) , where @xmath372 is a binary relation on @xmath269 :    1 .   for all @xmath118,@xmath373 . 2 .   for all cr - basic forms @xmath1 and @xmath374 .    by lemma  [ la:4.4 ] , these statements imply @xmath375 , that is , @xmath376 . assume @xmath376 . by lemma  [ la:2.12 ] , @xmath377 . by theorem  [ thm:1a ] , @xmath378 . by theorem  [ thm:4.8 ] , @xmath370 . hence , the relation @xmath367 is axiomatized by @xmath379 , and is thus a congruence . we now define a transformation on evaluation trees that mimics the function @xmath319 , and prove that equality of two such transformed trees characterizes the congruence that is axiomatized by @xmath379 . [ def:4.12 ] the unary * contractive evaluation function * @xmath380 yields * contractive evaluation trees * and is defined by @xmath381 the auxiliary function @xmath382 is defined as follows ( @xmath53 ) : @xmath383 for @xmath53 , the auxiliary functions @xmath384 and @xmath385 are defined by @xmath386 and @xmath387    as a simple example we depict @xmath388 and the contractive evaluation tree @xmath389 : @xmath286{ll } \begin{array}[t]{l } \\[-4 mm ] \begin{tikzpicture}[level distance=7.5 mm , level 1/.style={sibling distance=30 mm } , level 2/.style={sibling distance=15 mm } , level 3/.style={sibling distance=7.5 mm } ] \node ( a ) { $ a$ }    child { node ( b1 ) { $ a$ }      child { node ( c1 ) { $ a$ }        child { node ( d1 ) { $ { \ensuremath{{\sf t}}}$ } }         child { node ( d2 ) { $ { \ensuremath{{\sf f}}}$ } }      }      child { node ( c2 ) { $ { \ensuremath{{\sf f}}}$ }      }    }    child { node ( b2 ) { $ { \ensuremath{{\sf f}}}$ }     } ; \end{tikzpicture } \end{array } & \qquad \begin{array}[t]{l } \\[-4 mm ] \qquad \begin{tikzpicture}[level distance=7.5 mm , level 1/.style={sibling distance=30 mm } , level 2/.style={sibling distance=15 mm } , level 3/.style={sibling distance=7.5 mm } ] \node ( a ) { $ a$ }      child { node ( c1 ) { $ { \ensuremath{{\sf t}}}$ }    }    child { node ( b2 ) { $ { \ensuremath{{\sf f}}}$ }    } ; \end{tikzpicture } \\[8 mm ] \end{array}\end{array}\ ] ]    the similarities between the evaluation function @xmath390 and the function @xmath319 can be exploited , and we use the following lemma in the proof of the next completeness result .    [ la:4.13 ] for all @xmath88 , @xmath391 . we first prove the following auxiliary result : @xmath392 we prove the first equality by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath207 , let @xmath293 . we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath393 if @xmath107 , then @xmath394    the second equality can be proved in a similar way , and this finishes our proof of  . the lemma s statement now follows by a case distinction on @xmath1 . the cases @xmath103 follow immediately , and otherwise @xmath207 , and thus @xmath395    finally , we relate conditional statements by means of their contractive evaluation trees . [ def:4.14 ] * contractive valuation congruence * , notation @xmath396 , is defined on @xmath34as follows : @xmath397    the following characterization result immediately implies that @xmath396 is a congruence relation on @xmath269 ( and hence justifies calling it a congruence ) .    [ prop:4.15 ] for all @xmath118 , @xmath398 .    in order to prove @xmath120 , assume @xmath399 , thus @xmath400 . by corollary  [ cor:1 ] , @xmath401 , so by lemma  [ la:4.13 ] , @xmath402 . by lemma  [ la:2.6 ] and auxiliary result ( see the proof of lemma  [ la:3.5 ] ) , it follows that @xmath403 , that is , @xmath376 .    in order to prove @xmath122 , assume @xmath376 , thus @xmath403 and @xmath402 . by lemma  [ la:4.13 ] , @xmath401 . by corollary  [ cor:1 ] , @xmath305 and @xmath306 , so @xmath400 , that is , @xmath404 .    our final result in this section is a completeness result for contractive valuation congruence . [ thm:4.16 ] for all @xmath118 , @xmath405    combine theorem  [ thm:4.10 ] and proposition  [ prop:4.15 ] . in  @xcite we introduced @xmath406 , _ memorizing @xmath13 _ , as the extension of @xmath13  with the following axiom : @xmath407 axiom   expresses that the first evaluation value of @xmath16 is memorized . more precisely , a  memorizing evaluation " is one with the property that upon the evaluation of a compound propositional statement , the first evaluation value of each atom is memorized throughout the evaluation . we write @xmath406 for the set @xmath408 of axioms .    replacing the variable @xmath16 in axiom   by @xmath409 and/or the variable @xmath410 by @xmath411 yields all other memorizing patterns : @xmath412 furthermore , if we replace in axiom   @xmath410 by @xmath45 , we find the _ contraction law _ @xmath413 and replacing @xmath16 by @xmath409 then yields the dual contraction law @xmath414 hence , @xmath406 is an axiomatic extension of @xmath379 . we define a proper subset of basic forms with the property that each propositional statement can be proved equal to such a basic form . [ def:5.1 ] let @xmath415 be a subset of a. * mem - basic forms over @xmath415 * are inductively defined :    * @xmath25  and @xmath9  are mem - basic forms over @xmath415 , and * @xmath416 is a mem - basic form over @xmath415 if @xmath417 and @xmath1 and @xmath2 are mem - basic forms over @xmath418 . @xmath1 is a * mem - basic form * if for some @xmath419 , @xmath1 is a mem - basic form over @xmath415 .    note that if @xmath26 is finite , the number of mem - basic forms is also finite . it will turn out useful to define a function that transforms conditional statements into mem - basic forms . [ def:5.2 ] the * mem - basic form function * @xmath420 is defined by @xmath421 the auxiliary function @xmath422 is defined as follows : @xmath423 for @xmath53 , the auxiliary functions @xmath424 and @xmath425 are defined by @xmath426 and @xmath427    thus , @xmath428 maps a conditional statement @xmath1 to @xmath144 and then transforms @xmath144 according to the auxiliary functions @xmath429 , @xmath430 , and @xmath431 . we will use the following equalities . [ la:5.3 ] for all @xmath432 with @xmath433 and @xmath88 , @xmath434    by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath435 we have to distinguish three cases :    1 . if @xmath436 , then equality   follows by @xmath437 and equality   follows by @xmath438 equalities   and   can be proved in a similar way . 2 .   if @xmath439 , then equality   follows by @xmath440 and equality   follows by @xmath441 equalities   and   can be proved in a similar way . 3 .   if @xmath442 , then equality   follows by @xmath443 equalities @xmath444 can be proved in a similar way . [ la:5.4 ] for all @xmath53 and @xmath88 , @xmath445 and @xmath446 . fix some @xmath53 . we prove these inequalities by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath193 we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath447 and @xmath448 follows in a similar way .    if @xmath107 , then @xmath449 and @xmath450 follows in a similar way . [ la:5.5 ] for all @xmath30 , @xmath451 is a mem - basic form . we first prove an auxiliary result : @xmath452 this follows by induction on the depth @xmath87 of @xmath1 . if @xmath204 , then @xmath103 , and hence @xmath453 is a mem - basic form . for the inductive case @xmath206 it must be the case that @xmath207 . we find @xmath454 which is a mem - basic form because by lemma  [ la:5.4 ] , @xmath455 and @xmath456 are basic forms with depth smaller than or equal to @xmath211 , so by the induction hypothesis , @xmath457 is a mem - basic form over @xmath458 and @xmath459 is a mem - basic form over @xmath460 for suitable subsets @xmath458 and @xmath460 of @xmath26 . notice that by definition of @xmath430 and @xmath431 we can assume that the atom @xmath19 does not occur in @xmath461 . hence , @xmath462 is a mem - basic form over @xmath463 , which completes the proof of  . the lemma s statement now follows by structural induction : the base cases ( comprising a single atom @xmath19 ) are again trivial , and for the inductive case , @xmath464 for some basic form @xmath94 by lemma  [ la : bf ] , and by  , @xmath465 is a mem - basic form . the following lemma is used in proposition  [ prop:5.7 ] and lemma  [ la:5.8 ] . [ la:5.6 ] if @xmath224 is a mem - basic form , then @xmath466 and @xmath467 . assume @xmath224 is a mem - basic form over @xmath415 . by definition , @xmath2 and @xmath7 are mem - basic forms over @xmath468 . we prove both pairs of equalities simultaneously by induction on the structure of @xmath2 and @xmath7 . the base case , thus @xmath228 , is trivial .    if @xmath341 and @xmath342 , then @xmath469 and @xmath470 . moreover , the @xmath98 are mem - basic forms over @xmath471 , hence @xmath472 and @xmath473 , and thus @xmath474 the equalities for @xmath7 follow in a similar way .    if @xmath351 and @xmath352 , the lemma s equalities follow in a similar way , and this is also the case if @xmath214 and @xmath353 . with lemma  [ la:5.6 ] we can easily prove the following result . [ prop:5.7 ] for each @xmath30 , @xmath451 is a mem - basic form , and for each mem - basic form @xmath1 , @xmath475 . the first statement is lemma  [ la:5.5 ] . for the second statement , it suffices by lemma  [ la:2.12 ] to prove that @xmath453 . we prove this by case distinction on @xmath1 . the cases @xmath103 follow immediately , and otherwise @xmath104 , so @xmath476 . by lemma  [ la:5.6 ] , @xmath477 and @xmath478 , hence @xmath453 . [ la:5.8 ] for all @xmath88 , @xmath479 . we apply structural induction on @xmath1 . the base cases @xmath103 are trivial . assume @xmath104 . by induction @xmath480 . furthermore , by auxiliary result   in the proof of lemma  [ la:5.5 ] , @xmath481 is a mem - basic form , and @xmath482 are mem - basic forms over @xmath483 , and thus @xmath484 we derive @xmath485    [ thm:5.9 ] for all @xmath30 , @xmath486 .    by theorem  [ thm:1a ] and corollary  [ cor:1 ] , @xmath487 , and by lemma  [ la:5.8 ] , @xmath488 , and @xmath489 . [ def:5.10 ] the binary relation @xmath490 on @xmath34is defined as follows : @xmath491    [ thm:5.11 ] for all @xmath118 , @xmath492 . assume @xmath493 . then , by theorem  [ thm:5.9 ] , @xmath494 . in  @xcite the following two statements are proved ( theorem  8.1 and lemma  8.4 ) , where @xmath495 is a binary relation on @xmath269 :    1 .   for all @xmath118,@xmath496 . 2 .   for all mem - basic forms @xmath1 and @xmath497 .    by lemma  [ la:5.5 ] these statements imply @xmath498 , that is , @xmath499 . assume @xmath499 . by lemma  [ la:2.12 ] , @xmath500 . by theorem  [ thm:1a ] , @xmath501 . by theorem  [ thm:5.9 ] , @xmath493 . hence , the relation @xmath490 is axiomatized by @xmath406 and is thus a congruence . we define a transformation on evaluation trees that mimics the function @xmath428 , and prove that equality of two such transformed trees characterizes the congruence that is axiomatized by @xmath406 . [ def:5.12 ] the unary * memorizing evaluation function * @xmath502 yields * memorizing evaluation trees * and is defined by @xmath503 the auxiliary function @xmath504 is defined as follows ( @xmath53 ) : @xmath505 for @xmath53 , the auxiliary functions @xmath506 and @xmath507 are defined by @xmath508 and @xmath509    as a simple example we depict @xmath510 and the memorizing evaluation tree @xmath511 : @xmath512 \node ( a ) { $ a$ }    child { node ( b1 ) { $ b$ }      child { node ( c1 ) { $ a$ }        child { node ( d1 ) { $ { \ensuremath{{\sf t}}}$ } }         child { node ( d2 ) { $ { \ensuremath{{\sf f}}}$ } }      }      child { node ( c2 ) { $ { \ensuremath{{\sf f}}}$ }      }    }    child { node ( b2 ) { $ { \ensuremath{{\sf f}}}$ }    } ; \end{tikzpicture } \end{array } & \qquad \begin{array}{l } \qquad \begin{tikzpicture}[level distance=7.5 mm , level 1/.style={sibling distance=30 mm } , level 2/.style={sibling distance=15 mm } , level 3/.style={sibling distance=7.5 mm } ] \node ( a ) { $ a$ }    child { node ( b1 ) { $ b$ }      child { node ( c1 ) { $ { \ensuremath{{\sf t}}}$ }      }      child { node ( c2 ) { $ { \ensuremath{{\sf f}}}$ }      }    }    child { node ( b2 ) { $ { \ensuremath{{\sf f}}}$ }    } ; \end{tikzpicture } \\[8 mm ] \end{array}\end{array}\ ] ]    the similarities between @xmath513 and the function @xmath428 will of course be exploited .    [ la:5.13 ] for all @xmath432 with @xmath433 and @xmath288 ,    * @xmath514 , * @xmath515 , * @xmath516 , * @xmath517 .    by structural induction on @xmath41 ( cf . the proof of lemma  [ la:5.3 ] ) . we use the following lemma s in the proof of our next completeness result . [ la:5.14 ] for all @xmath53 and @xmath88 , @xmath518    we first prove an auxiliary result : @xmath519 fix some @xmath53 . we prove   by structural induction on @xmath1 . the base cases @xmath103 are trivial . for the inductive case @xmath193 we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath520 and if @xmath107 , then @xmath521 this finishes the proof of  . we now prove the lemma s equalities . fix some @xmath53 . we prove the first equality by induction on @xmath87 . the base case @xmath204 , thus @xmath103 , is trivial . for the inductive case @xmath206 , it must be the case that @xmath193 . we have to distinguish the cases @xmath194 and @xmath107 . if @xmath194 , then @xmath522 if @xmath107 , then @xmath523    the second equality can be proved in a similar way . [ la:5.15 ] for all @xmath88 , @xmath524 .    by a case distinction on @xmath1 . the cases @xmath103 follow immediately , and otherwise @xmath207 , and thus @xmath525    [ def:5.16 ] * memorizing valuation congruence * , notation @xmath526 , is defined on @xmath34as follows : @xmath527    the following characterization result immediately implies that @xmath526 is a congruence relation on @xmath269 ( and hence justifies calling it a congruence ) . [ prop:5.17 ] for all @xmath118 , @xmath528 .    for @xmath120 , assume @xmath529 , thus @xmath530 . by corollary  [ cor:1 ] , @xmath531 so by lemma  [ la:5.15 ] , @xmath532 by lemma  [ la:2.6 ] , it follows that @xmath533 , that is , @xmath499 .    in order to prove @xmath122 , assume @xmath499 , thus @xmath533 . then @xmath534 and by lemma  [ la:5.15 ] , @xmath535 by corollary  [ cor:1 ] , @xmath530 , that is , @xmath536 . we end this section with a completeness result for memorizing valuation congruence . [ thm:5.18 ] for all @xmath118 , @xmath537    combine theorem  [ thm:5.11 ] and proposition  [ prop:5.17 ] . the most identifying axiomatic extension of @xmath13  we consider can be defined by adding the following axiom to @xmath406 : @xmath538 so , the evaluation value of each atom in a conditional statement is memorized , and by axiom  , no atom @xmath19 can have a side effect because @xmath539 for all @xmath30 . we write @xmath540 for the set of these axioms , thus @xmath541 observe that the duality principle also holds in @xmath540 , in particular , @xmath542 . a simple example on @xmath540 illustrates how the order of evaluation of @xmath17 and @xmath16 can be swapped : @xmath543 equation   can be derived as follows : @xmath544    the following lemma is a direct consequence of axiom  . [ la:6.1 ] for all @xmath118 , @xmath545 . @xmath546    in  @xcite we defined @xmath547 as the extension of @xmath13  with the following two axioms : @xmath548 axiom expresses how the order of evaluation of @xmath410 and @xmath16 can be swapped , and ( as explained section  [ sec : mem ] ) the contraction law   expresses that the evaluation result of @xmath16 is memorized . because we will rely on results for @xmath547 that are proven in  @xcite , we first prove the following result . [ prop:3 ] the axiom sets @xmath549 and @xmath540 are equally strong . we show that all axioms in the one set are derivable from the other set . we first prove that the axiom   is derivable from @xmath549 : @xmath550 where the contraction law  , that is @xmath551 , is derivable from @xmath549 : replace @xmath16 by @xmath409 in  . hence @xmath552 . furthermore , if we take @xmath553 in axiom   we find @xmath554 , hence @xmath555 .    in order to show that @xmath556 recall that the contraction law   is derivable from @xmath406 ( see section  [ sec : mem ] ) . so , it remains to be proved that @xmath557 and with equation   we can easily derive this axiom from @xmath540 : @xmath558    given a finite , ordered subset of atoms we define a proper subset of basic forms with the property that each propositional statement over these atoms can be proved equal to such a basic form .    [ def:6.3 ] let @xmath559 be the set of strings over @xmath26 with the property that each @xmath560 contains no multiple occurrences of the same atom . for the empty string , thus @xmath561 . ] * st - basic forms over @xmath562 * are defined as follows :    * @xmath25  and @xmath9  are st - basic forms over @xmath563 . * @xmath416 is an st - basic form over @xmath564 if @xmath1 and @xmath2 are st - basic forms over @xmath565 . @xmath1 is an * st - basic form * if for some @xmath560 , @xmath1 is an st - basic form over @xmath78 . for example , an st - basic form over @xmath566 has the following form : @xmath567 with @xmath568 . for @xmath569 , there exist @xmath570 different st - basic forms over @xmath78 . it will turn out useful to define a function that transforms conditional statements to st - basic forms . therefore , given @xmath562 we consider terms in @xmath571 , where @xmath415 is the finite subset of @xmath26 that contains the elements of @xmath78 . if @xmath64 , then @xmath572 and the st - basic forms over @xmath563 are @xmath25  and @xmath9 .    [ def:6.4 ] the * alphabet function * @xmath573 returns the set of atoms of a string in @xmath574 : @xmath575    [ def:6.5 ] let @xmath562 . the conditional statement @xmath576 is defined as @xmath577 the * st - basic form function * @xmath578 is defined by @xmath579    so , for each @xmath562 , @xmath580 is an st - basic form over @xmath78 in which the constant @xmath25  does not occur , e.g. , @xmath581    [ la:6.6 ] let @xmath562 . for all @xmath30 , @xmath582 .    by induction on the structure of @xmath78 . if @xmath64 , then @xmath583 and @xmath584 if @xmath585 for some @xmath586 and @xmath53 , then @xmath587 , and hence @xmath588    [ la:6.7 ] let @xmath562 . for all @xmath589 , @xmath590 is an st - basic form . we use two auxiliary results : @xmath591.\end{aligned}\ ] ] this easily follows by induction on the structure of @xmath78 . @xmath592)=e^\rho[{\ensuremath{{\sf f}}}\mapsto\ell_a({\ensuremath{\mathit{bf}}}(p))]\\[1 mm ] \text{and~}~{r}_a((e^\rho[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(p)])=e^\rho[{\ensuremath{{\sf f}}}\mapsto{r}_a({\ensuremath{\mathit{bf}}}(p ) ) ] , \end{array}\end{aligned}\ ] ] both equalities follow easily by induction on the structure of @xmath565 . we prove the lemma s statement by induction on the structure of @xmath78 . if @xmath64 , then @xmath1 contains no atoms . hence , @xmath593 . if @xmath160 then @xmath594 which is an st - basic form over @xmath563 , and similarly for the case @xmath163 . if @xmath585 for some @xmath586 and @xmath53 , we derive @xmath595 ) & & \text{by~\eqref{aux : s1}}\\ & = { \ensuremath{\mathit{mf}}}((e^\rho{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}e^\rho)[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(p)])\\ & = { \ensuremath{\mathit{mf}}}(e^\rho[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(p)]{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}e^\rho[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(p)])\\ & = { \ensuremath{\mathit{mf}}}(\ell_{a}(e^\rho[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(p)])){{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}{\ensuremath{\mathit{mf}}}({r}_{a}(e^\rho[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(p ) ] ) ) \\ & = { \ensuremath{\mathit{mf}}}(e^\rho[{\ensuremath{{\sf f}}}\mapsto\ell_{a}({\ensuremath{\mathit{bf}}}(p))]){{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}{\ensuremath{\mathit{mf}}}(e^\rho[{\ensuremath{{\sf f}}}\mapsto{r}_{a}({\ensuremath{\mathit{bf}}}(p ) ) ] ) & & \text{by~\eqref{aux : s2}}\\ & = { \ensuremath{\mathit{mf}}}(e^\rho[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}(\ell_{a}({\ensuremath{\mathit{bf}}}(p)))]){{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}{\ensuremath{\mathit{mf}}}(e^\rho[{\ensuremath{{\sf f}}}\mapsto{\ensuremath{\mathit{bf}}}({r}_{a}({\ensuremath{\mathit{bf}}}(p ) ) ) ] ) & & \text{by lemma~\ref{la:2.12}}\\ & = { \ensuremath{\mathit{mf}}}({\ensuremath{\mathit{bf}}}({\ensuremath{{\sf t}}}{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}e^\rho{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}\ell_{a}({\ensuremath{\mathit{bf}}}(p)))){{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}{\ensuremath{\mathit{mf}}}({\ensuremath{\mathit{bf}}}({\ensuremath{{\sf t}}}{{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}e^\rho{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}{r}_{a}({\ensuremath{\mathit{bf}}}(p ) ) ) ) & & \text{by~\eqref{aux : s1}}\\ & = { \ensuremath{\mathit{sbf}}}_\rho(\ell_{a}({\ensuremath{\mathit{bf}}}(p))){{\raisebox{0pt}{\footnotesize$\;\triangleleft~$}}}a{{\raisebox{0pt}{\footnotesize$~\triangleright\;$}}}{\ensuremath{\mathit{sbf}}}_\rho({r}_{a}({\ensuremath{\mathit{bf}}}(p))),\end{aligned}\ ] ] where the penultimate equality follows by   applied to @xmath565 because @xmath596 and @xmath597 are conditional statements in @xmath598 ( thus , not containing @xmath19 ) . by induction , @xmath599 and @xmath600 are st - basic forms over @xmath565 . hence , @xmath590 is an st - basic form over @xmath78 . [ la:6.8 ] let @xmath562 . for all @xmath589 , @xmath601 . by lemma  [ la:6.6 ] , @xmath582 . by theorem  [ thm:5.9 ] , @xmath602 , hence @xmath601 . [ thm:6.9 ] let @xmath562 . for all @xmath603 , @xmath604 . assume @xmath605 . then , by lemma  [ la:6.8 ] , @xmath606 , and by proposition  [ prop:3 ] , @xmath607 . in  @xcite the following two statements are proved ( theorem  9.1 and an auxiliary result in its proof ) , where @xmath608 is a binary relation on @xmath269 :    1 .   for all @xmath118,@xmath609 . 2 .   for all st - basic forms @xmath1 and @xmath610 .    by lemma  [ la:6.7 ] these statements imply @xmath611 . assume @xmath611 , and thus @xmath612 . by theorem  [ thm:5.11 ] , @xmath613 , and by lemma  [ la:6.6 ] this implies @xmath605 . [ def:6.11 ] let @xmath562 . the binary relation @xmath614 on @xmath615 is defined as follows : @xmath616    [ thm:6.12 ] let @xmath562 . for all @xmath603 , @xmath617 . assume @xmath605 . by lemma  [ la:6.8 ] , @xmath606 , and by theorem  [ thm:6.9 ] , @xmath618 . assume @xmath618 , and thus @xmath611 . by theorem  [ thm:6.9 ] , @xmath619 . hence , the relation @xmath614 is a congruence on @xmath615 that is axiomatized by @xmath540 . we define a transformation on evaluation trees that mimics the function @xmath620 and prove that equality of two such transformed trees characterizes the congruence that is axiomatized by @xmath540 . [ def:6.13 ] let @xmath562 . the unary * static evaluation function * @xmath621 yields * static evaluation trees * and is defined as follows : @xmath622 where @xmath580 is defined in definition  [ def:6.5 ] . [ ex : st ] let @xmath623 . we depict @xmath68 at the left - hand side . the static evaluation tree @xmath624 is depicted in the middle , and the static evaluation tree @xmath625 is depicted at the right - hand side : @xmath626 \node ( a ) { $ a$ }    child { node ( b1 ) { $ b$ }      child { node ( c1 ) { $ a$ }        child { node ( d1 ) { $ { \ensuremath{{\sf t}}}$ } }         child { node ( d2 ) { $ { \ensuremath{{\sf f}}}$ } }      }      child { node ( c2 ) { $ { \ensuremath{{\sf f}}}$ }      }    }    child { node ( b2 ) { $ { \ensuremath{{\sf t}}}$ }    } ; \end{tikzpicture } \end{array } & \qquad \begin{array}{l } \qquad \begin{tikzpicture}[level distance=7.5 mm , level 1/.style={sibling distance=15 mm } , level 2/.style={sibling distance=7.5 mm } , level 3/.style={sibling distance=7.5 mm } ] \node ( a ) { $ a$ }    child { node ( b1 ) { $ b$ }      child { node ( c1 ) { $ { \ensuremath{{\sf t}}}$ }      }      child { node ( c2 ) { $ { \ensuremath{{\sf f}}}$ }      }    }    child { node ( b2 ) { $ b$ }      child { node ( c3 ) { $ { \ensuremath{{\sf t}}}$ }      }      child { node ( c4 ) { $ { \ensuremath{{\sf t}}}$ }      }    } ; \end{tikzpicture } \\[8 mm ] \end{array } & \qquad \begin{array}{l } \qquad \begin{tikzpicture}[level distance=7.5 mm , level 1/.style={sibling distance=15 mm } , level 2/.style={sibling distance=7.5 mm } , level 3/.style={sibling distance=7.5 mm } ] \node ( a ) { $ b$ }    child { node ( b1 ) { $ a$ }      child { node ( c1 ) { $ { \ensuremath{{\sf t}}}$ }      }      child { node ( c2 ) { $ { \ensuremath{{\sf t}}}$ }      }    }    child { node ( b2 ) { $ a$ }      child { node ( c3 ) { $ { \ensuremath{{\sf f}}}$ }      }      child { node ( c4 ) { $ { \ensuremath{{\sf t}}}$ }      }    } ; \end{tikzpicture } \\[8 mm ] \end{array } \end{array}\ ] ] the two different static evaluation trees correspond to the different ways in which one can present truth tables for @xmath1 , that is , the different possible orderings of the valuation values of the atoms occurring in @xmath1 : @xmath627 _ end example . _ the reason that @xmath628 is defined relative to some @xmath562 that covers the alphabet of @xmath1 is that in order to prove completeness of @xmath540 ( and @xmath547 ) , we need to be able to relate conditional statements that contain different sets of atoms , such as for example @xmath629 and that have equal static evaluation trees . for @xmath630 and @xmath631 the static evalution trees for example   are @xmath632 and @xmath633 , thus @xmath634 \node ( a ) { $ a$ }    child { node ( b1 ) { $ b$ }      child { node ( c1 ) { $ { \ensuremath{{\sf f}}}$ }      }      child { node ( c2 ) { $ { \ensuremath{{\sf f}}}$ }      }    }    child { node ( b2 ) { $ b$ }      child { node ( c3 ) { $ { \ensuremath{{\sf f}}}$ }      }      child { node ( c4 ) { $ { \ensuremath{{\sf f}}}$ }      }    } ; \end{tikzpicture } \end{array } & \qquad \begin{array}{l } \qquad \begin{tikzpicture}[level distance=7.5 mm , level 1/.style={sibling distance=30 mm } , level 2/.style={sibling distance=15 mm } , level 3/.style={sibling distance=7.5 mm } ] \node ( a ) { $ b$ }    child { node ( b1 ) { $ a$ }      child { node ( c1 ) { $ { \ensuremath{{\sf f}}}$ }      }      child { node ( c2 ) { $ { \ensuremath{{\sf f}}}$ }      }    }    child { node ( b2 ) { $ a$ }      child { node ( c3 ) { $ { \ensuremath{{\sf f}}}$ }      }      child { node ( c4 ) { $ { \ensuremath{{\sf f}}}$ }      }    } ; \end{tikzpicture } \end{array } \end{array}\ ] ]    the similarities between @xmath635 and the function @xmath620 can be exploited and lead to our final completeness result . [ def:6.15 ] let @xmath560 . * static valuation congruence over @xmath78 * , notation @xmath636 , is defined on @xmath615 as follows : @xmath637    the following characterization result immediately implies that for all @xmath562 , @xmath636 is a congruence relation on @xmath615 . [ prop:6.14 ] let @xmath562 . for all @xmath603 , @xmath638 we have to show @xmath639 and this immediately follows from proposition  [ prop:5.17 ] .    [ thm:6.15 ] let @xmath560 . for all @xmath603 , @xmath640 combine theorem  [ thm:6.12 ] and proposition  [ prop:6.14 ] . in  @xcite we introduced proposition algebra using hoare s conditional @xmath641 and the constants @xmath8 and @xmath45 . we defined a number of varieties of so - called _ valuation algebras _ in order to capture different semantics for the evaluation of conditional statements , and provided axiomatizations for the resulting valuation congruences : @xmath642 ( four axioms ) characterizes the least identifying valuation congruence we consider , and the extension @xmath406 ( one extra axiom ) characterizes the most identifying valuation congruence below propositional logic , while static valuation congruence , axiomatized by adding the simple axiom @xmath554 to @xmath406 , can be seen as a characterization of propositional logic . in  @xcite we introduced an alternative valuation semantics for proposition algebra in the form of _ hoare - mccarthy algebras _ ( hma s ) that is more elegant than the semantical framework provided in  @xcite : hma - based semantics has the advantage that one can define a valuation congruence without first defining the valuation _ equivalence _ it is contained in .    in this paper , we use staudt s evaluation trees  @xcite to define free valuation congruence as the relation @xmath111 ( see section  [ sec : free ] ) , and this appears to be a relatively simple and stand - alone exercise , resulting in a semantics that is elegant and much simpler than hma - based semantics  @xcite and the semantics defined in  @xcite . by theorem  [ thm:1 ] , @xmath111 coincides with `` free valuation congruence as defined in  @xcite '' because both relations are axiomatized by @xmath642 ( see ( * ? ? ? * thm.4.4 and thm.6.2 ) ) . the advantage of `` evaluation tree semantics '' is that for a given conditional statement @xmath1 , the evaluation tree @xmath68 determines all relevant evaluations , so @xmath123 is determined by evaluation trees that contain no more atoms than those that occur in @xmath1 and @xmath2 , which corresponds to the use of truth tables in propositional logic .    in section  [ sec : rp ] we define repetition - proof valuation congruence @xmath297 on @xmath269 by @xmath307 if , and only if @xmath300 , where @xmath643 and @xmath644 is a transformation function on evaluation trees . it is obvious that this transformation is `` natural '' , given the axiom schemes @xmath645 and that are characteristic for @xmath173 . the equivalence on @xmath269 that we want to prove is @xmath646 by which @xmath297 coincides with `` repetition - proof valuation congruence as defined in  @xcite '' because both are axiomatized by @xmath173 ( see ( * ? ? ? * thm.6.3 ) ) . however , equivalence   implies that @xmath297 is a _ congruence _ relation on @xmath34  and we could not find a direct proof of this fact . we chose to simulate the transformation @xmath287 by the transformation @xmath187 on conditional statements and to prove that the resulting equivalence relation @xmath263 is a congruence axiomatized by @xmath173 . this is theorem  [ thm:3.11 ] , the proof of which depends on  ( * ? ? ? * thm.6.3 ) ) _ and _ on theorem  [ thm:3.9 ] , that is , @xmath647 in order to prove equivalence   ( which is theorem  [ thm:3.17 ] ) , it is thus sufficient to prove that @xmath263 and @xmath297 coincide , and this is proposition  [ prop:3.16 ] . the structure of our proofs on the axiomatizations of the other valuation congruences that we consider is very similar , although the case for static valuation congruence requires a slightly more complex proof ( below we return to this point ) . moreover , these axiomatizations are incremental : the axiom systems @xmath173 up to and including @xmath540 all share the axioms of @xmath13 , and each succeeding system is defined by the addition of either one or two axioms , in most cases making previously added axiom(s ) redundant . given some @xmath562 , this implies that in @xmath615 , @xmath648 where all these inclusions are proper if @xmath649 , and thus @xmath650 , and thus @xmath651 . we conclude that repetition - proof evaluation trees and the valuation congruence @xmath297 provide a full - fledged , simple and elegant semantics for @xmath173 , and that this is also the case for contractive evaluation trees and the valuation congruence @xmath396 , and memorizing evaluation trees and the valuation congruence @xmath526 . static valuation congruence over @xmath615 for some @xmath562 , coincides with any standard semantics of propositional logic in the following sense : @xmath652 where @xmath653 and @xmath654 refer to hoare s definition  @xcite : @xmath655 let @xmath53 . the fact that @xmath656 identifies more than @xmath526 is immediately clear : @xmath657 while it is easy to see that @xmath658 . our proof that @xmath540 , and thus @xmath547 is an axiomatization of static valuation congruence is slightly more complex than those for the other axiomatizations because evaluation of a conditional statement @xmath1 does not enforce a canonical order for the evaluation of its atoms , and therefore such an ordering as encoded by a static evaluation tree should be fixed beforehand . to this purpose , we use some @xmath562 .    a spin - off of our approach can be called `` basic form semantics for proposition algebra '' : for each valuation congruence c considered , two conditional statements are c - valuation congruent if , and only if , they have equal c - basic forms , where c - basic forms are obtained by a syntactic transformation of conditional statements , which is a form of normalization . it is cumbersome , but not difficult to prove that given some @xmath562 , the function @xmath620 is a normalization function on @xmath615 . in addition to lemma  [ la:6.7 ] this requires proving that for each st - basic form @xmath1 over @xmath78 , @xmath659 . we conclude with a brief digression on _ short - circuit logic _ , which we defined in  @xcite ( see  @xcite for a quick introduction ) , and an example on the use of @xmath173 . familiar binary connectives that occur in the context of imperative programming and that prescribe short - circuit evaluation , such as ` & & ` ( in c called `` logical and '' ) , are often defined in the following way : @xmath660 independent of the precise syntax of @xmath1 and @xmath2 , hence , @xmath661 . in a similarly way , negation can be defined by @xmath662 . short - circuit logic focuses on the question @xmath663 a first approach to this question is to adopt the conditional as an auxiliary operator , as is done in  @xcite , and to answer question   using definitions of the binary propositional connectives as above and the axiomatization for the valuation congruence of interest in proposition algebra ( or , if `` mixed conditional statements '' are at stake , axiomatizations for the appropriate valuations congruences ) . an alternative and more direct approach to question   is to establish axiomatizations for short - circuited binary connectives in which the conditional is _ not _ used . for free valuation congruence , an equational axiomatization of short - circuited binary propositional connectives is provided by staudt in  @xcite , where @xmath664 $ ] and @xmath665 $ ] ( and @xmath51 is also defined for short - circuited disjunction ) , and the associated completeness proof is based on decomposition properties of such evaluation trees . for repetition - proof valuation congruence it is an open question whether a finite , equational axiomatization of the short - circuited binary propositional connectives exists , and an investigation of repetition - proof evaluation trees defined by such connectives might be of interest in this respect . we conclude with an example on the use of @xmath173 that is based on  ( * ? ? ? * ex.4 ) . [ ex : rp2 ] let @xmath26 be a set of atoms of the form ` ( e==e ' ) ` and ` ( n = e ) ` with @xmath666 some initialized program variable and @xmath667 arithmetical expressions over the integers that may contain @xmath666 . assume that ` ( e==e ' ) ` evaluates to @xmath10  if @xmath668 and @xmath669 represent the same value , and ` ( n = e ) ` always evaluates to _ true _ with the effect that @xmath668 s value is assigned to @xmath666 . then these atoms satisfy the axioms of @xmath173 . follow from @xmath173 , e.g. , @xmath670 . we note that a particular consequence of @xmath173 in the setting of short - circuit logic is @xmath671 ( cf . example  [ ex : rp ] ) , and that example  [ ex : rp2 ] is related to the work of wortel  @xcite , where an instance of _ propositional dynamic logic _ @xcite is investigated in which assignments can be turned into tests ; the assumption that such tests always evaluate to _ true _ is natural because the assumption that assignments always succeed is natural . ] notice that if @xmath666 has initial value 0 or 1 , @xmath672 and @xmath673 evaluate to different results , so the atom ` ( n = n+1 ) ` does not satisfy the law @xmath674 , by which this example is typical for the repetition - proof characteristic of @xmath173 . _ end example . _    we finally note that all valuation congruences considered in this paper can be used as a basis for systematic analysis of the kind of _ side effects _ that may occur upon the evaluation of short - circuited connectives as in example  [ ex : rp ] , and we quote these words of parnas  @xcite :    _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ `` most mainline methods disparage side effects as a bad programming practice . yet even in well - structured , reliable software , many components do have side effects ; side effects are very useful in practice . it is time to investigate methods that deal with side effects as the normal case . '' _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _              bergstra , j.a . and ponse , a. ( 2012 ) . proposition algebra and short - circuit logic . in f. arbab and m. sirjani ( eds . ) , _ proceedings of the 4th international conference on fundamentals of software engineering _ ( fsen 2011 ) , tehran . volume 7141 of lecture notes in computer science , pages 15 - 31 . springer - verlag .
proposition algebra is based on hoare s conditional connective , which is a ternary connective comparable to if - then - else and used in the setting of propositional logic . 
 conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so - called free valuation congruence : two conditional statements are free valuation congruent if , and only if , they have equal evaluation trees . 
 free valuation congruence is axiomatized by the four basic equational axioms of proposition algebra that define the conditional connective . 
 valuation congruences that identify more conditional statements than free valuation congruence are repetition - proof , contractive , memorizing , and static valuation congruence . 
 each of these valuation congruences is characterized using a transformation on evaluation trees : two conditional statements are c - valuation congruent if , and only if , their c - transformed evaluation trees are equal . 
 these transformations are simple and natural , and only for static valuation congruence a slightly more complex transformation is used . 
 also , each of these valuation congruences is axiomatized in proposition algebra . a spin - off of our approach 
 is `` basic form semantics for proposition algebra '' : for each valuation congruence c considered , two conditional statements are c - valuation congruent if , and only if , they have equal c - basic forms , where c - basic forms are obtained by a syntactic transformation of conditional statements , which is a form of normalization . 
 conditional composition , evaluation tree , proposition algebra , short - circuit evaluation , side effect