(** Uniform bulk composition for
    1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA.
    This is a local transition theorem, not a blank-start nonhalting proof.
    AI assistance: GPT-6 Astra (OpenAI). *)

From BusyCoq Require Import Individual62.
From AstraLocal Require Import LocalRules.
Require Import Lia List.
Open Scope list.

Lemma bulk_left l r n :
  l <* (rev Qblk)^^n <{{A}} r -->* l <{{A}} Pblk^^n *> r.
Proof.
  shift_rule. intros. apply progress_evstep, bulk_left_one.
Qed.

Lemma bulk_right l r n :
  l <* (rev Wguard) {{C}}> Pblk^^n *> r -->*
  l <* (rev Rblk)^^n <* (rev Wguard) {{C}}> r.
Proof.
  shift_rule. intros. apply progress_evstep, bulk_right_one.
Qed.

Lemma guard_rotation n l :
  (rev Rblk)^^n *> (rev Gguard) *> l =
  (rev Gguard) *> (rev Qblk)^^n *> l.
Proof.
  induction n.
  - reflexivity.
  - cbn [lpow]. rewrite !Str_app_assoc. rewrite IHn.
    change ((rev Rblk ++ rev Gguard) *> (rev Qblk)^^n *> l =
            (rev Gguard ++ rev Qblk) *> (rev Qblk)^^n *> l).
    reflexivity.
Qed.

Theorem bulk_roundtrip l r n :
  l <* (rev Gguard) <* (rev Wguard) {{C}}>
    Pblk^^n *> Ttail *> [0;0;0;0;0;0;0;0] *> r -->+
  l <{{A}} Pblk^^(n+2) *> Ttail *> r.
Proof.
  follow bulk_right.
  rewrite guard_rotation.
  follow10 right_reflection.
  follow bulk_left.
  rewrite lpow_add. simpl_tape. finish.
Qed.

Print Assumptions bulk_roundtrip.