Require Import Sib.W43core.
From BusyCoq Require Import Individual62.
Require Import List NArith.
Import ListNotations.
Fixpoint chunks (n : nat) (c : cfg) : list cfg :=
  match n with O => [c] | S n' => match runp 500000 c with Some (c', _) => c :: chunks n' c' | None => [c] end 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.
Eval native_compute in map pr (chunks 37 (Rc B ([], T0) ([], T0))).
Eval native_compute in map pr (chunks 37 (Rc F ([], T0) ([], T0))).