Require Import Sib.W43core.
From BusyCoq Require Import Individual62.
Require Import List NArith.
Import ListNotations.
Definition R28f : list (bool * N) := [(true, 224495); (true, 673559); (true, 7); (true, 9841); (true, 1942040); (false, 2)]%N.
Fixpoint leq (a : list run) (b : list (bool * N)) : bool :=
  match a, b with
  | [], [] => true
  | (s, n) :: a', (s', m) :: b' => andb (Bool.eqb (seqb s S1) s') (andb (N.eqb (lc n) m) (andb (Nat.eqb (length (lv n)) 0) (leq a' b')))
  | _, _ => false
  end.
Definition tgt (c : cfg) : bool :=
  match c with
  | Rc B (_, T0) (r, T0) => leq r R28f
  | _ => false
  end.
Definition step1 (c : cfg) (k : N) : bool * cfg * N :=
  if tgt c then (true, c, k) else
  match sstep c with Some (c', _) => (false, c', N.succ k) | None => (true, c, k) end.
Fixpoint go (p : positive) (c : cfg) (k : N) : bool * cfg * N :=
  match p with
  | xH => step1 c k
  | xO p' => let '(f, c1, k1) := go p' c k in if f then (f, c1, k1) else go p' c1 k1
  | xI p' => let '(f, c0, k0) := step1 c k in if f then (f, c0, k0) else
             let '(f1, c1, k1) := go p' c0 k0 in if f1 then (f1, c1, k1) else go p' c1 k1
  end.
Definition qn (q : Q) : nat := match q with A => 0 | B => 1 | C => 2 | D => 3 | E => 4 | F => 5 end.
Definition sd_pr (s : sd) := (map (fun x => (seqb (fst x) S1, lc (snd x), length (lv (snd x)))) (fst s), match snd s with T0 => true | _ => false end).
Definition pr (c : cfg) := match c with Rc q l r => (true, qn q, sd_pr l, sd_pr r) | Lc q l r => (false, qn q, sd_pr l, sd_pr r) end.
Definition res (q : Q) := let '(f, c, k) := go 33554431 (Rc q ([], T0) ([], T0)) 0 in (f, k, pr c).
Eval native_compute in res A.
Eval native_compute in res B.
Eval native_compute in res F.