Fine Points
lTo be perfectly
rigorous, weĠd need to axiomatize information
such as:
length([A | X]) == 1 + length(X)
lWeĠd want to formalize the definition of length, addition, etc.
lThere are software systems such as ACL2 that automate many proofs of this nature.
length([A | X]) == 1 + length(X)
lWeĠd want to formalize the definition of length, addition, etc.
lThere are software systems such as ACL2 that automate many proofs of this nature.