Direct word equality at the original resource bounds

Plain word leaves feed a reachable-prefix fold. Both encoded inputs are charged, with the original product time bound and linear workspace bound; no higher tidy calculus is imported.

theorem Turing.MultiTapeTM.ComputableInDegree.eqWordsStep : ComputableInDegree (fun (q : (List Bool × Bool) × Bool) => EqWords.step q.1 q.2) (encPair (encPair encBits encBool) encBool) (encPair encBits encBool) 1 1

A step of comparing words.

theorem Turing.MultiTapeTM.ComputableInDegree.eqWordsResult : ComputableInDegree (fun (s : List Bool × Bool) => s.2 && s.1.isEmpty) (encPair encBits encBool) encBool 1 0

The result of comparing words, from the state after the last step.

theorem Turing.MultiTapeTM.ComputableInO.eqWords : ComputableInO (fun (p : List Bool × List Bool) => decide (p.1 = p.2)) (encPair encBits encBits) encBool (fun (p : List Bool × List Bool) => (p.1.length + 1) * (p.1.length + p.2.length + 1)) fun (p : List Bool × List Bool) => p.1.length + p.2.length + 1

Equality of words, within the length of the first word times the length of both, and linear space.

theorem Turing.MultiTapeTM.ComputableInO.eq {α : Type} [DecidableEq α] (enc : α ↪ List Bool) : ComputableInO (fun (p : α × α) => decide (p.1 = p.2)) (encPair enc enc) encBool (fun (p : α × α) => ((enc p.1).length + 1) * ((enc p.1).length + (enc p.2).length + 1)) fun (p : α × α) => ((encPair enc enc) p).length

Equality, for any encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_eq' {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [_inst4 : DecidableEq β] {left right : α → β} (hleft : ComputableInPolyTime left encA encB) (hright : ComputableInPolyTime right encA encB) : ComputableInPolyTime (fun (x : α) => decide (left x = right x)) encA encBool

Compare computed values for equality, inferring their common encoding from the arguments.

theorem Turing.MultiTapeTM.ComputableInPolyTime.beq {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [BEq β] [LawfulBEq β] {left right : α → β} (hleft : ComputableInPolyTime left encA encB) (hright : ComputableInPolyTime right encA encB) : ComputableInPolyTime (fun (x : α) => left x == right x) encA encBool

Lawful Boolean equality compares computed values through their common encoding.