fact: Fixpoint memo_get_val (l : list cube) (m : MStream) {struct l} : A := match l with nil => match m with MSeq (mval a) _ _ _ _ _ _ _ => a end | C1 :: l1 => match m with MSeq _ m1 _ _ _ _ _ _ => memo_get_val l1 m1 end | C2 :: l1 => match m with MSeq _ _ m1 _ _ _ _ _ => memo_get_val l1 m1 end | C3 :: l1 => match m with MSeq _ _ _ m1 _ _ _ _ => memo_get_val l1 m1 end | C4 :: l1 => match m with MSeq _ _ _ _ m1 _ _ _ => memo_get_val l1 m1 end | C5 :: l1 => match m with MSeq _ _ _ _ _ m1 _ _ => memo_get_val l1 m1 end | C6 :: l1 => match m with MSeq _ _ _ _ _ _ m1 _ => memo_get_val l1 m1 end | C7 :: l1 => match m with MSeq _ _ _ _ _ _ _ m1 => memo_get_val l1 m1 end end.
imports: PrimInt63 Cyclic63 List BasicRubik