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.
New to topics? Read the docs here!