fun perim(W, L) => add(mul(W, 2), mul(L, 2))
fun main() => perim(50, 33)

rule mul_comm(mul(A, B)) => mul(B, A)
rule add_comm(add(A, B)) => add(B, A)

theorem
    perim_comm(perim(W, L)) => perim(L, W)
proof
    *perim_expand(perim(W, L))
    add(mul(W, 2), mul(L, 2))
    *add_comm(add(mul(W, 2), mul(L, 2)))
    add(mul(L, 2), mul(W, 2))
    *perim_contract(add(mul(L, 2), mul(W, 2)))
    perim(L, W)
qed