Word comparison by a left fold

The original comparison state and its all-word laws, independent of resource certificates.

def Turing.MultiTapeTM.EqWords.step (s : List Bool × Bool) (b : Bool) : List Bool × Bool

One step of comparing a word with s.1, the part of the other word still to be matched; s.2 records whether the words agree so far.

theorem Turing.MultiTapeTM.EqWords.foldl_fst (l r : List Bool) (ok : Bool) : (List.foldl step (r, ok) l).fst = List.drop l.length r

theorem Turing.MultiTapeTM.EqWords.foldl_result (l r : List Bool) (ok : Bool) : ((List.foldl step (r, ok) l).snd && (List.foldl step (r, ok) l).fst.isEmpty) = (ok && decide (l = r))