Equational reasoning
= Equational reasoning
Prove equality of expressions through a chain of substitutions justified by definitions, previously established equalities, or algebraic laws. Each step preserves the expression's value. In a <programming language> with <lazy evaluation>, an asserted program law must also preserve termination and the demanded amount of a partial value, not just agree on finite defined inputs.