The right strategy when confronted like a goal such as
LENGTH (APP [] l2) = LENGTH [] + LENGTH l2
is to look at the sub-terms that contain patterns that “should” be simpler.
When I look at the above, I see
APP [] l2
and
LENGTH []
You have equational theorems to hand that have terms mat
Good morning,
I’m currently taking a class where HOL is used but not taught via example and
solution, this in turn has swayed my interest in HOL until I found the 2017
lecture on the hol-theorem-prover website. I’ve been stuck on what the TA for
the class says “Is an easy question and help isn’
