proposition: Lemma eval_to_sss_compute n i (P : list (bsm_instr n)) c (v : vec (list bool) n) c' v' : eval n (i, P) (c, v) (c', v') -> sss_compute (@bsm_sss _) (i,P) (c, v) (c', v').
proof: Proof. generalize (i, P) as iP. generalize (c, v) as cv. generalize (c', v') as c'v'. clear. induction 1 as [ i P c v | i P c v j b c' v' H1 H2 H [k IH] | i P c v j c1 c2 c' v' l H1 H2 H3 H [k IH] | i P c v j c1 c2 c' v' l H1 H2 H3 H [k IH] | i P c v j c1 c2 c' v' H1 H2 H3 H [k IH] ]. - exists 0. econstructor. - exists (1 + k). eapply nth_error_split in H2 as (l1 & l2 & -> & Hl). repeat econstructor. + f_equal. lia. + now replace (1 + c) with (c + 1) by lia. - exists (1 + k). eapply nth_error_split in H2 as (l1 & l2 & -> & Hl). econstructor; [ | eauto]. repeat econstructor. + f_equal. lia. + replace (c + 1) with (1 + c) by lia. econstructor. eauto. - exists (1 + k). eapply nth_error_split in H2 as (l1 & l2 & -> & Hl). econstructor; [ | eauto]. repeat econstructor. * f_equal. lia. * eauto. - exists (1 + k). eapply nth_error_split in H2 as (l1 & l2 & -> & Hl). econstructor; [ | eauto]. repeat econstructor. + f_equal. lia. + eauto. Qed.
imports: Undecidability.StackMachines.BSM List Bool Lia Nat Undecidability.Shared.Libs.DLW(list_bool pos vec sss)