Overview of the Proof of a Trivial Consequence

ACL2 !>(defthm trivial-consequence
         (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
                (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))

ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...): The previously added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application.

By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture to

Goal' (EQUAL (APP X1 (APP X2 (APP X3 (APP X4 (APP X5 (APP X6 X7)))))) (APP X1 (APP X2 (APP X3 (APP X4 (APP X5 (APP X6 X7))))))).

But we reduce the conjecture to T, by primitive type reasoning.

Q.E.D.

Summary Form: ( DEFTHM TRIVIAL-CONSEQUENCE ...) Rules: ((:REWRITE ASSOCIATIVITY-OF-APP) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume Time: 0.20 seconds (prove: 0.02, print: 0.00, other: 0.18) TRIVIAL-CONSEQUENCE

You might explore the links before moving on.