Checks for the application of Associativity at the top level.
(We call these the target and the source, but because rules of
replacement apply in both directions, we could use the same rule
to go from the target to the source as we use to go from the source
to the target.)
p V (q V r) ==> (p V q) V r ==> p V (q V r)
(p & q) & r ==> p & (q & r) ==> (p & q) & r
Checks for the application of Associativity at the top level.
(We call these the target and the source, but because rules of replacement apply in both directions, we could use the same rule to go from the target to the source as we use to go from the source to the target.)
p V (q V r) ==> (p V q) V r ==> p V (q V r) (p & q) & r ==> p & (q & r) ==> (p & q) & r