Side dependence for string functions

A lattice of side-dependence predicates over List.DependsOn: BoundedDependence f s says a single margin caps the influence of side s at every output coordinate, TwoSidedUnboundedDependence places one target under the influence of both sides, and RequiresBothSides demands both sides at once. flankWord is the witness family instantiating the negative side: a target buried in a filler run between two independently editable flanks. The non-interacting bimachines — the weak-determinism class of [MMBMcC24], whose cell output is an order-independent union of one-sided change-rules over the identity — live here with their exclusion and separation theorems.

Main definitions

• LeftDetermined f i: output coordinate i is fixed by the prefix Set.Iic i
• BoundedDependence f s, UnboundedDependence f s: whether one margin caps the influence of side s at every output coordinate
• TwoSidedUnboundedDependence f: for every d, one base word carries a target flipped by far perturbations on either side
• RequiresBothSides f: the target is changed, and either far perturbation alone reverts it
• OneSidedChanges f: every changed cell is determined by one side of its input alone
• flankWord x fill y n: a target buried in a filler run with editable flanks
• Bimachine.NonInteraction, Bimachine.IsNonInteracting: the cell output decomposed as an order-independent union of one-sided change-rules over the identity
• IsNonInteractingBimachineComputable f: f is computed by some non-interacting finite bimachine

Main theorems

• unboundedDependence_iff: every margin fails at some output coordinate
• RequiresBothSides.of_flanks: the three-map witness template — a map is excluded by three target-cell observations
• IsNonInteractingBimachineComputable.oneSidedChanges: a non-interacting bimachine changes each cell from one side
• IsLeftSubsequential.boundedDependence_right: a length-preserving left-subsequential function depends boundedly on the right
• Mealy.leftDetermined, Mealy.boundedDependence_right: a sequential machine is prefix-determined at every coordinate
• RequiresBothSides.not_isNonInteractingBimachineComputable: a map whose target needs both sides at once is computed by no non-interacting bimachine
• setOf_isNonInteractingBimachineComputable_ssubset: the non-interacting class is proper inside the bimachine-computable functions

Implementation notes

The coordinate predicates index the output coordinate and the input window separately, which is informative for length-preserving functions; for block-emitting transducers the two drift apart. BoundedDependence is the positive primitive; unboundedDependence_iff recovers the margin-indexed witness form, and unpacking ¬ List.DependsOn yields word-pair witnesses. The forms are margin-indexed rather than fixed-index because a fixed target has only finitely many positions to its left. The predicates place no in-range guard on target coordinates: for length-preserving maps an out-of-range coordinate is none on both sides of any perturbation.

The dependence lattice

def LeftDetermined {α : Type u_1} {β : Type u_2} (f : List α → List β) (i : ℕ) : Prop

Output coordinate i is fixed by the prefix Set.Iic i.

Equations

• LeftDetermined f i = List.DependsOn (fun (u : List α) => (f u)[i]?) (Set.Iic i)

def IsFarPerturbation {α : Type u_1} (base u : List α) (i d : ℕ) (s : ScanDirection) : Prop

An equal-length variant of base differing only beyond the d-margin of target i on side s.

Equations

• IsFarPerturbation base u i d s = (u.length = base.length ∧ Set.EqOn (fun (x : ℕ) => base[x]?) (fun (x : ℕ) => u[x]?) (s.window i d))

def BoundedDependence {α : Type u_1} {β : Type u_2} (f : List α → List β) (s : ScanDirection) : Prop

f depends boundedly on side s: a single margin caps, at every output coordinate, how far input on side s can matter.

Equations

• BoundedDependence f s = ∃ (N : ℕ), ∀ (i : ℕ), List.DependsOn (fun (u : List α) => (f u)[i]?) (s.window i N)

def UnboundedDependence {α : Type u_1} {β : Type u_2} (f : List α → List β) (s : ScanDirection) : Prop

f depends unboundedly on side s.

Equations

• UnboundedDependence f s = ¬BoundedDependence f s

@[simp]

theorem not_unboundedDependence_iff {α : Type u_1} {β : Type u_2} {f : List α → List β} {s : ScanDirection} : ¬UnboundedDependence f s ↔ BoundedDependence f s

f fails unbounded dependence on side s exactly when its dependence there is bounded.

theorem unboundedDependence_iff {α : Type u_1} {β : Type u_2} {f : List α → List β} {s : ScanDirection} : UnboundedDependence f s ↔ ∀ (N : ℕ), ∃ (i : ℕ), ¬List.DependsOn (fun (u : List α) => (f u)[i]?) (s.window i N)

Unbounded dependence coordinate-wise: every margin fails at some output coordinate.

theorem BoundedDependence.right_of_leftDetermined {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : ∀ (i : ℕ), LeftDetermined f i) : BoundedDependence f ScanDirection.right

A map whose every output coordinate is fixed by its prefix Set.Iic i depends boundedly on the right.

theorem BoundedDependence.right_of_prefixDetermined {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : ∀ (i : ℕ), List.DependsOn (fun (u : List α) => (f u)[i]?) (Set.Iio i)) : BoundedDependence f ScanDirection.right

A map whose every output coordinate is fixed by the input's strict prefix Set.Iio i depends boundedly on the right.

def TwoSidedUnboundedDependence {α : Type u_1} {β : Type u_2} (f : List α → List β) : Prop

For every d, one base word carries a target whose output flips under a far perturbation on either side.

Equations

• TwoSidedUnboundedDependence f = ∀ (d : ℕ), ∃ (base : List α), ∃ i < base.length, ∀ (s : ScanDirection), ∃ (u : List α), IsFarPerturbation base u i d s ∧ (f base)[i]? ≠ (f u)[i]?

theorem TwoSidedUnboundedDependence.unboundedDependence {α : Type u_1} {β : Type u_2} {f : List α → List β} (h : TwoSidedUnboundedDependence f) (s : ScanDirection) : UnboundedDependence f s

Co-located two-sided dependence yields unbounded dependence on either side.

def RequiresBothSides {α : Type u_1} (f : List α → List α) : Prop

f requires both sides when some target changes under f yet perturbing either far side reverts it to the identity.

Equations

• One or more equations did not get rendered due to their size.

def OneSidedChanges {α : Type u_1} (f : List α → List α) : Prop

Every changed cell is determined by the input on one side of it alone — which side may vary from cell to cell.

Equations

• OneSidedChanges f = ∀ (w : List α) (i : ℕ), (f w)[i]? ≠ w[i]? → ∃ (s : ScanDirection), List.DependsAt (fun (u : List α) => (f u)[i]?) (s.window i 0) w

theorem RequiresBothSides.not_oneSidedChanges {α : Type u_1} {f : List α → List α} (hf : RequiresBothSides f) : ¬OneSidedChanges f

A map that requires both sides has a change no single side determines.

theorem RequiresBothSides.twoSidedUnboundedDependence {α : Type u_1} {f : List α → List α} (hf : RequiresBothSides f) : TwoSidedUnboundedDependence f

Requiring both sides strengthens two-sided unbounded dependence.

The flank-witness template

The recurring witness family for two-sided unboundedness: a target buried in a filler run, with independently editable flanks. RequiresBothSides.of_flanks packages the whole assembly — a map is excluded by three target-cell observations: the base image leaves the filler, and either single-flank perturbation restores it.

def flankWord {α : Type u_1} (x fill y : α) (n : ℕ) : List α

The word x, then n copies of fill, then y.

Equations

• flankWord x fill y n = x :: (List.replicate n fill ++ [y])

@[simp]

theorem length_flankWord {α : Type u_1} {x fill y : α} {n : ℕ} : (flankWord x fill y n).length = n + 2

theorem getElem?_flankWord {α : Type u_1} {x fill y : α} {n k : ℕ} : (flankWord x fill y n)[k]? = if k = 0 then some x else if k = n + 1 then some y else if k < n + 2 then some fill else none

@[simp]

theorem getElem?_flankWord_zero {α : Type u_1} {x fill y : α} {n : ℕ} : (flankWord x fill y n)[0]? = some x

@[simp]

theorem getElem?_flankWord_last {α : Type u_1} {x fill y : α} {n : ℕ} : (flankWord x fill y n)[n + 1]? = some y

theorem getElem?_flankWord_mid {α : Type u_1} {x fill y : α} {n k : ℕ} (h₁ : 0 < k) (h₂ : k ≤ n) : (flankWord x fill y n)[k]? = some fill

theorem getElem?_flankWord_eq_some_iff {α : Type u_1} {x fill y a : α} {n j : ℕ} (hfill : fill ≠ a) : (flankWord x fill y n)[j]? = some a ↔ j = 0 ∧ x = a ∨ j = n + 1 ∧ y = a

A non-filler value sits only on a flank.

theorem take_flankWord {α : Type u_1} {x fill y : α} {n k : ℕ} (hk : k ≤ n) : List.take (k + 1) (flankWord x fill y n) = x :: List.replicate k fill

The window up to the filler run is the left flank and part of the run.

theorem drop_flankWord {α : Type u_1} {x fill y : α} {n k : ℕ} (hk : k ≤ n) : List.drop (k + 1) (flankWord x fill y n) = List.replicate (n - k) fill ++ [y]

The window past the left flank is the rest of the run and the right flank.

theorem mem_take_flankWord_iff {α : Type u_1} {x fill y a : α} {n k : ℕ} (hfill : fill ≠ a) (hk : k ≤ n) : a ∈ List.take (k + 1) (flankWord x fill y n) ↔ x = a

A window reaching at most the filler run contains a iff the left flank is a.

theorem mem_drop_flankWord_iff {α : Type u_1} {x fill y a : α} {n k : ℕ} (hfill : fill ≠ a) (hk : k ≤ n) : a ∈ List.drop (k + 1) (flankWord x fill y n) ↔ y = a

A window past the left flank contains a iff the right flank is a.

theorem any_take_flankWord {α : Type u_1} {x fill y : α} {n k : ℕ} {p : α → Bool} (hfill : p fill = false) (hk : k ≤ n) : (List.take (k + 1) (flankWord x fill y n)).any p = p x

A flag over a window reaching at most the filler run reads the left flank.

theorem any_drop_flankWord {α : Type u_1} {x fill y : α} {n k : ℕ} {p : α → Bool} (hfill : p fill = false) (hk : k ≤ n) : (List.drop (k + 1) (flankWord x fill y n)).any p = p y

A flag over a window past the left flank reads the right flank.

theorem IsFarPerturbation.flankWord_left {α : Type u_1} {x fill y : α} {n i d : ℕ} (x' : α) (h : d < i) : IsFarPerturbation (flankWord x fill y n) (flankWord x' fill y n) i d ScanDirection.left

Changing only the left flank perturbs beyond the d-margin of a target past it.

theorem IsFarPerturbation.flankWord_right {α : Type u_1} {x fill y : α} {n i d : ℕ} (y' : α) (h : i + d ≤ n) : IsFarPerturbation (flankWord x fill y n) (flankWord x fill y' n) i d ScanDirection.right

Changing only the right flank perturbs beyond the d-margin of a target d-clear of the last position.

theorem TwoSidedUnboundedDependence.of_flanks {α : Type u_1} {β : Type u_2} {f : List α → List β} {fill xOn yOn xOff yOff : α} {n t : ℕ → ℕ} (ht : ∀ (d : ℕ), d < t d) (hn : ∀ (d : ℕ), t d + d ≤ n d) (hL : ∀ (d : ℕ), (f (flankWord xOn fill yOn (n d)))[t d]? ≠ (f (flankWord xOff fill yOn (n d)))[t d]?) (hR : ∀ (d : ℕ), (f (flankWord xOn fill yOn (n d)))[t d]? ≠ (f (flankWord xOn fill yOff (n d)))[t d]?) : TwoSidedUnboundedDependence f

A d-indexed family of flank words whose target's image flips under changing either flank alone has two-sided unbounded dependence.

theorem RequiresBothSides.of_flanks {α : Type u_1} {f : List α → List α} {fill xOn yOn xOff yOff : α} {n t : ℕ → ℕ} (ht : ∀ (d : ℕ), d < t d) (hn : ∀ (d : ℕ), t d + d ≤ n d) (hchange : ∀ (d : ℕ), (f (flankWord xOn fill yOn (n d)))[t d]? ≠ some fill) (hrevL : ∀ (d : ℕ), (f (flankWord xOff fill yOn (n d)))[t d]? = some fill) (hrevR : ∀ (d : ℕ), (f (flankWord xOn fill yOff (n d)))[t d]? = some fill) : RequiresBothSides f

A d-indexed family of flank words whose target sits d-far from both flanks, changed in the base and reverted by flipping either flank alone, requires both sides.

Non-interacting bimachines: the apparatus

Non-interacting decompositions

def Bimachine.OneSidedAt {α : Type u_1} {β : Type u_2} {L : Type u_3} {R : Type u_4} (B : Bimachine L R α β) (l : L) (a : α) (r : R) : Prop

The output at a cell is determined by one side alone: fixing the input symbol and one context state already fixes it.

Equations

• B.OneSidedAt l a r = ((∀ (r' : R), B.output l a r' = B.output l a r) ∨ ∀ (l' : L), B.output l' a r = B.output l a r)

def Bimachine.unite {α : Type u_1} [DecidableEq α] (cL cR a : α) : α

unite cL cR a takes the left proposal if it fires (≠ a), else the right one — the union of two change proposals over the identity default a. The tie-break is asymmetric (when both fire the left wins) but inert under the order-independence IsNonInteracting requires.

Equations

• Bimachine.unite cL cR a = if cL = a then cR else cL

@[simp]

theorem Bimachine.unite_right_self {α : Type u_1} [DecidableEq α] (cL a : α) : unite cL a a = cL

With the right proposal inert, the union is whatever the left one proposes.

@[simp]

theorem Bimachine.unite_left_self {α : Type u_1} [DecidableEq α] (cR a : α) : unite a cR a = cR

With the left proposal inert, the union is whatever the right one proposes.

theorem Bimachine.unite_of_left_ne {α : Type u_1} [DecidableEq α] {cL a : α} (h : cL ≠ a) (cR : α) : unite cL cR a = cL

A firing left proposal wins.

theorem Bimachine.unite_comm_iff {α : Type u_1} [DecidableEq α] {cL cR a : α} : unite cL cR a = unite cR cL a ↔ cL ≠ a → cR ≠ a → cL = cR

The union is order-independent exactly when the proposals agree wherever both fire.

@[simp]

theorem Bimachine.unite_eq_self_iff {α : Type u_1} [DecidableEq α] {cL cR a : α} : unite cL cR a = a ↔ cL = a ∧ cR = a

The combined value is the default exactly when both one-sided proposals are inert.

structure Bimachine.NonInteraction {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] (B : Bimachine L R α α) : Type (max (max u_1 u_3) u_4)

A non-interacting decomposition of a bimachine: a change-rule per side over the identity default, whose union is order-independent and produces the cell output.

• ruleL : L → α → α

  The change the left context proposes for the current symbol.

• ruleR : R → α → α

  The change the right context proposes for the current symbol.

• unite_comm (l : L) (a : α) (r : R) : unite (self.ruleL l a) (self.ruleR r a) a = unite (self.ruleR r a) (self.ruleL l a) a

  The union of the two proposals is order-independent (unite_comm_iff: they agree wherever both fire), so neither side can suppress the other's change.

• output_eq (l : L) (a : α) (r : R) : B.output l a r = [unite (self.ruleL l a) (self.ruleR r a) a]

  The cell output is the union of the two proposals.

def Bimachine.IsNonInteracting {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] (B : Bimachine L R α α) : Prop

A bimachine over a single alphabet is non-interacting when it admits a non-interacting decomposition (NonInteraction) of its cell output.

Equations

• B.IsNonInteracting = Nonempty B.NonInteraction

def Bimachine.NonInteraction.letterToLetter {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {B : Bimachine L R α α} (w : B.NonInteraction) : B.LetterToLetter

A non-interacting decomposition exhibits the bimachine as letter-to-letter.

Equations

• w.letterToLetter = { cell := fun (l : L) (a : α) (r : R) => Bimachine.unite (w.ruleL l a) (w.ruleR r a) a, output_eq := ⋯ }

theorem Bimachine.NonInteraction.output_eq_ruleL {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {B : Bimachine L R α α} (w : B.NonInteraction) {l : L} {a : α} {r : R} (hL : w.ruleL l a ≠ a) : B.output l a r = [w.ruleL l a]

A firing left rule alone determines the output.

theorem Bimachine.NonInteraction.output_eq_ruleR {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {B : Bimachine L R α α} (w : B.NonInteraction) {l : L} {a : α} {r : R} (hR : w.ruleR r a ≠ a) : B.output l a r = [w.ruleR r a]

A firing right rule alone determines the output — order-independence of the union is what silences the left state.

theorem Bimachine.NonInteraction.oneSidedAt_of_change {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {B : Bimachine L R α α} {l : L} {a : α} {r : R} (w : B.NonInteraction) (hne : B.output l a r ≠ [a]) : B.OneSidedAt l a r

At every cell whose output differs from the input symbol, a decomposed bimachine is one-sided: the change is the left rule's alone or the right rule's alone.

theorem Bimachine.IsNonInteracting.oneSidedAt_of_change {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {B : Bimachine L R α α} {l : L} {a : α} {r : R} (h : B.IsNonInteracting) (hne : B.output l a r ≠ [a]) : B.OneSidedAt l a r

At every cell whose output differs from the input symbol, a non-interacting bimachine is one-sided.

def Bimachine.NonInteraction.map {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {L' : Type u_5} {R' : Type u_6} {B : Bimachine L R α α} (w : B.NonInteraction) (eL : L ≃ L') (eR : R ≃ R') : (Bimachine.map eL eR B).NonInteraction

Transport a decomposition along state equivalences.

Equations

• w.map eL eR = { ruleL := fun (l : L') (a : α) => w.ruleL (eL.symm l) a, ruleR := fun (r : R') (a : α) => w.ruleR (eR.symm r) a, unite_comm := ⋯, output_eq := ⋯ }

theorem Bimachine.IsNonInteracting.map {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {L' : Type u_5} {R' : Type u_6} {B : Bimachine L R α α} (h : B.IsNonInteracting) (eL : L ≃ L') (eR : R ≃ R') : (Bimachine.map eL eR B).IsNonInteracting

Non-interaction transports along state reindexing.

theorem Bimachine.NonInteraction.getElem?_run_eq_iff {α : Type u_1} {L : Type u_3} {R : Type u_4} [DecidableEq α] {B : Bimachine L R α α} (w : B.NonInteraction) {a : α} {u : List α} {i : ℕ} (hsym : u[i]? = some a) : (B.run u)[i]? = u[i]? ↔ w.ruleL (B.lState (List.take i u)) a = a ∧ w.ruleR (B.rState (List.drop (i + 1) u)) a = a

A decomposed bimachine fixes cell i exactly when both change-proposals are inert at its two context states.

The non-interacting class

def IsNonInteractingBimachineComputable {α : Type u_1} [DecidableEq α] (f : List α → List α) : Prop

Computability by a non-interacting finite bimachine.

Equations

• IsNonInteractingBimachineComputable f = ∃ (L : Type) (x : Fintype L) (R : Type) (x : Fintype R) (B : Bimachine L R α α), B.run = f ∧ B.IsNonInteracting

theorem isNonInteractingBimachineComputable_iff {α : Type u_1} [DecidableEq α] {f : List α → List α} : IsNonInteractingBimachineComputable f ↔ ∃ (L : Type v) (x : Fintype L) (R : Type w) (x : Fintype R) (B : Bimachine L R α α), B.run = f ∧ B.IsNonInteracting

f is computed by a non-interacting finite bimachine if and only if it is computed by one with state types in any universes.

theorem Bimachine.isNonInteractingBimachineComputable {α : Type u_1} [DecidableEq α] {L : Type u_3} {R : Type u_4} [Fintype L] [Fintype R] (B : Bimachine L R α α) (h : B.IsNonInteracting) : IsNonInteractingBimachineComputable B.run

A non-interacting finite-state bimachine witnesses IsNonInteractingBimachineComputable for its run, whatever the universes of its state types (IsNonInteracting.map).

theorem IsBimachineComputable.of_nonInteracting {α : Type u_1} [DecidableEq α] {f : List α → List α} (h : IsNonInteractingBimachineComputable f) : IsBimachineComputable f

A function computed by a non-interacting bimachine is in particular bimachine-computable.

theorem IsNonInteractingBimachineComputable.length_eq {α : Type u_1} [DecidableEq α] {f : List α → List α} (h : IsNonInteractingBimachineComputable f) (x : List α) : (f x).length = x.length

Functions computed by non-interacting bimachines are length-preserving.

theorem IsNonInteractingBimachineComputable.of_mealyComputable {α : Type u_1} [DecidableEq α] {f : List α → List α} (h : IsMealyComputable f) : IsNonInteractingBimachineComputable f

A Mealy-computable function is computed by a non-interacting bimachine: the bimachine view (Mealy.toBimachine) has a trivial right automaton, so the cell output is a one-sided rule with ωR the identity.

Machines bound dependence

A length-preserving left-subsequential function depends boundedly on the right: the delay bound of IsLeftSubsequential.exists_getElem?_append_eq is the dependence bound. Sequential machines are the zero-delay case — prefix-determined at every coordinate (Mealy.leftDetermined), which is strictly stronger than bounded right dependence.

theorem IsLeftSubsequential.boundedDependence_right {α : Type u_1} {β : Type u_2} {f : List α → List β} (hlen : ∀ (w : List α), (f w).length = w.length) (hf : IsLeftSubsequential f) : BoundedDependence f ScanDirection.right

A length-preserving left-subsequential function depends boundedly on the right.

theorem Mealy.leftDetermined {α : Type u_1} {β : Type u_2} {σ : Type u_3} (T : Mealy σ α β) (i : ℕ) : LeftDetermined T.run i

A sequential machine is left-determined at every coordinate.

theorem Mealy.boundedDependence_right {α : Type u_1} {β : Type u_2} {σ : Type u_3} (T : Mealy σ α β) : BoundedDependence T.run ScanDirection.right

A sequential machine's output never depends on input to its right.

theorem IsMealyComputable.leftDetermined {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) (i : ℕ) : LeftDetermined f i

A Mealy-computable map is left-determined at every coordinate.

theorem IsMealyComputable.boundedDependence_right {α : Type u_1} {β : Type u_2} {f : List α → List β} (hf : IsMealyComputable f) : BoundedDependence f ScanDirection.right

A Mealy-computable map's output never depends on input to its right.

Non-interacting bimachines

A map that requires both sides escapes the non-interacting bimachines, and the conjunctive flag bimachine shows the non-interacting class is proper.

theorem RequiresBothSides.not_isNonInteractingBimachineComputable {α : Type u_1} [DecidableEq α] {f : List α → List α} (hf : RequiresBothSides f) : ¬IsNonInteractingBimachineComputable f

A map that requires both sides is computed by no non-interacting bimachine. At the witness the base changes but each far perturbation reverts: the right perturbation shares the left window, silencing ruleL at this cell; the left perturbation shares the right window, silencing ruleR; yet the base needs one of them to fire.

Strictness: non-interacting ⊊ bimachine-computable

A conjunctive change — a symbol raised iff a mark occurs on both sides — is bimachine-computable but requires both sides, so no non-interacting bimachine computes it.

def conjBM : Bimachine Bool Bool Bool Bool

The conjunctive flag bimachine: a false cell is raised exactly when a true occurs on both sides.

Equations

• conjBM = Bimachine.ofFlags id id fun (l s r : Bool) => s || l && r

theorem conjBM.run_flankWord_mid (x y : Bool) (d : ℕ) : (conjBM.run (flankWord x false y (2 * d + 1)))[d + 1]? = some (x && y)

In the middle of a d-margined flank word, conjBM computes the conjunction of the two flanks.

theorem conjBM.requiresBothSides : RequiresBothSides conjBM.run

The conjunctive change requires both sides: with a mark on each flank the medial cell is raised, and demoting either mark alone reverts it — the three-map template, one map per argument.

theorem IsNonInteractingBimachineComputable.oneSidedChanges {α : Type u_1} [DecidableEq α] {f : List α → List α} (hf : IsNonInteractingBimachineComputable f) : OneSidedChanges f

Changed cells of a non-interacting bimachine's run are each determined by a single side, OneSidedAt transported to words.

theorem setOf_isNonInteractingBimachineComputable_ssubset : {f : List Bool → List Bool | IsNonInteractingBimachineComputable f} ⊂ {f : List Bool → List Bool | IsBimachineComputable f}

The non-interacting class is proper inside the bimachine-computable functions — conjBM is computed by a bimachine, but by no non-interacting one.