proposition: Lemma sss_output_to_eval n i (P : list (bsm_instr n)) c (v : vec (list bool) n) c' v' : sss_output (@bsm_sss _) (i,P) (c, v) (c', v') -> eval n (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. intros ? ? ? [[k H1] H2]. induction H1 as [cv | n0 st1 st2 (c', v') (k & l & i & r & d & -> & -> & HH) H IH] in * |- *. - destruct iP as (i, P), cv as (c, v); try destruct c'v' as (c', v'). econstructor. cbn in *. lia. - revert IH H H2. inversion_clear HH as [ | | | ]; subst; intros IH' HHH IH % IH'; clear IH'. + eapply eval_bsm_pop_empty; [ lia | | eauto ..]. rewrite nth_error_app2; [ | lia]. now replace (k + length l - k - length l) with 0 by lia. + eapply eval_bsm_pop_false; [ lia | | eauto ..]. rewrite nth_error_app2; [ | lia]. now replace (k + length l - k - length l) with 0 by lia. + eapply eval_bsm_pop_true; [ lia | | eauto ..]. * rewrite nth_error_app2; [ | lia]. now replace (k + length l - k - length l) with 0 by lia. * now replace (k + length l + 1) with (1 + (k + length l)) by lia. + eapply eval_bsm_push; [ lia | | eauto ..]. * rewrite nth_error_app2; [ | lia]. now replace (k + length l - k - length l) with 0 by lia. * now replace (k + length l + 1) with (1 + (k + length l)) by lia. Qed.
imports: Undecidability.StackMachines.BSM List Bool Lia Nat Undecidability.Shared.Libs.DLW(list_bool pos vec sss)