(* The threshold network itself: started from the bits of a start state, its orbit holds the bits of the
   machine's state at every step, so it carries every generation of the organism, and from the K-th
   generation on it repeats every K generations. *)
From Stdlib Require Import List Bool Arith ZArith Lia.
Import ListNotations.
From TH Require Import TwoHead Organism PassCheck Run Main PhysSem PhysMain.

Section NetRing.
Variables (K S0 L : nat).
Hypotheses (HK : 2 <= K) (HS : G <= S0) (HL : length desc <= L).

Theorem network_reproduces : forall x0, start K S0 L x0 -> forall g, 1 <= g ->
  netiter 6 K S0 L (g * T S0) (encode 6 K S0 L x0) = encode 6 K S0 L (itern 6 K S0 L (g * T S0) x0)
  /\ after K S0 L x0 g (itern 6 K S0 L (g * T S0) x0).
Proof.
  intros x0 Hs g Hg. split; [|exact (reproduces K S0 L HK HS HL x0 Hs g Hg)].
  destruct Hs as (Hf & _).
  exact (network_orbit 6 K S0 L (g * T S0) x0 ltac:(lia) HK (HS1' K S0 L HK HS HL) (HL1 K S0 L HK HS HL) Hf).
Qed.

Theorem network_periodic : forall x0, start K S0 L x0 -> forall g, K <= g ->
  netiter 6 K S0 L ((g + K) * T S0) (encode 6 K S0 L x0) = netiter 6 K S0 L (g * T S0) (encode 6 K S0 L x0).
Proof.
  intros x0 Hs g Hg. pose proof Hs as (Hf & _).
  rewrite !(network_orbit 6 K S0 L _ x0 ltac:(lia) HK (HS1' K S0 L HK HS HL) (HL1 K S0 L HK HS HL) Hf).
  rewrite (periodic K S0 L HK HS HL x0 Hs g Hg). reflexivity.
Qed.

End NetRing.