>quite clearly you had formal proofs which do not meet the symbolic abstraction requirements

I've been unable to imagine or recall an example. Can you provide one?