(* The netlist of ternary threshold units computes the ring machine: every orbit of the network on
   encoded states is the encoding of an orbit of the machine. *)
From Stdlib Require Import List Bool Arith ZArith Lia.
Import ListNotations.
From TH Require Import TwoHead Net Gates Phys PhysWF PhysSem.

(* the network iterated on its state bits *)
Fixpoint netiter (al K S0 L n : nat) (x : list bool) : list bool :=
  match n with
  | O => x
  | S m => netiter al K S0 L m (netstep (nst al K S0 L) (phys_units al K S0 L) (phys_next al K S0 L) x)
  end.

Lemma itern_fits : forall al K S0 L n s, 4 <= al -> 2 <= K -> 1 <= S0 -> 1 <= L ->
  fits al K S0 L s -> fits al K S0 L (itern al K S0 L n s).
Proof.
  intros al K S0 L n. induction n as [|n IH]; intros s Hal HK HS HL Hs; [exact Hs|].
  cbn [itern]. apply IH; try assumption. apply step_fits; assumption.
Qed.

(* From every state of the machine with a window of 2^al cells, al >= 4, K >= 2 banks of S0 >= 1 slots
   and K tapes of L >= 1 cells, the network started from the encoded state holds after n steps the
   encoding of the state the machine reaches in n steps. *)
Theorem network_orbit : forall al K S0 L n s, 4 <= al -> 2 <= K -> 1 <= S0 -> 1 <= L -> fits al K S0 L s ->
  netiter al K S0 L n (encode al K S0 L s) = encode al K S0 L (itern al K S0 L n s).
Proof.
  intros al K S0 L n. induction n as [|n IH]; intros s Hal HK HS HL Hs; [reflexivity|].
  cbn [netiter itern]. rewrite (netlist_step al K S0 L s Hal HK HS HL Hs).
  apply IH; try assumption. apply step_fits; assumption.
Qed.