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'].
Time Eval vm_compute in reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 74806 598752)], TV 0) (Re_r5, T0)) (Lc D ([], TV 0) (Rs_r0, T0)).
Time Eval vm_compute in reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 24910 199584)], TV 0) (Re_r0, T0))
  (Lc D (nb (tl1 673560 5388768) (tl1 224496 1796256) (tl1 74805 598752) (tl1 24910 199584), TV 0) (Rs_r1, T0)).
Time Eval vm_compute in reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 673558 5388768)] ++ comp_runs [tl1 56123 449064; tl1 18701 149688; tl1 6227 49896; tl1 2069 16632] (blk U0), TV 0) (Re_r1, T0)) (Lc D ([], TV 0) (Rs_r2, T0)).
Time Eval vm_compute in reach 100000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (Re_r2, T0))
  (Lc D (nb (tl1 74808 598752) (tl1 24912 199584) (tl1 8277 66528) xv, TV 0) (Rs_r3, T0)).
Time Eval vm_compute in reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 74806 598752)], TV 0) (Re_r3, T0)) (Lc D ([], TV 0) (Rs_r4, T0)).
Time Eval vm_compute in reach 100000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (Re_r4, T0))
  (Lc D (nb (tl1 673560 5388768) (tl1 224496 1796256) (tl1 74805 598752) xv, TV 0) (sub9 Rs_r5, T0)).