Require Import ssim chain count right.
From BusyCoq Require Import Individual62.
Require Import List NArith.
Import ListNotations.
Definition res (c : cfg) := urun 100000 c.
Definition shw (c : cfg) := match c with
  | Lc q (l, tl) (r, tr) => (true, q, map (fun r => (fst r, lc (snd r), lv (snd r))) l, map (fun r => (fst r, lc (snd r), lv (snd r))) r)
  | Rc q (l, tl) (r, tr) => (false, q, map (fun r => (fst r, lc (snd r), lv (snd r))) l, map (fun r => (fst r, lc (snd r), lv (snd r))) r) end.
Definition sub9 (rs : list run) : list run := map (fun r => (fst r, match lv (snd r) with [a] => LF (lc (snd r) + a)%N [(9 * a)%N] | _ => snd r end)) rs.
Definition xv : lf := LF 2 [0%N; 4%N].
Definition nb (t' s' a' l' : lf) : list run := mkruns S0 [cn 3; t'; s'; a'; l'].
Fixpoint find (n : nat) (c : cfg) : option cfg :=
  match n with O => None | S n' =>
    match c with
    | Lc D (l, TV O) r => if Nat.eqb (length l) 5 then Some c else match sstep c with Some (c', _) => find n' c' | None => None end
    | _ => match sstep c with Some (c', _) => find n' c' | None => None end
    end end.
Definition shwo (o : option cfg) := match o with Some c => shw c | None => shw (Rc A ([], T0) ([], T0)) end.
Eval vm_compute in shwo (find 5000 (Rc B ([(S0, cn 1); (S0, tl1 24910 199584)], TV 0) (Re_r0, T0))).
Eval vm_compute in shwo (find 5000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (Re_r2, T0))).
Eval vm_compute in shwo (find 5000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (Re_r4, T0))).
Eval vm_compute in (Rs_r1, Rs_r3, sub9 Rs_r5).