proposition: Fact main_init_spec v : (i,main_init) // (i,v) ->> (13+i,v[(Zero::nil)/s][nil/a][nil/h][nil/l]).
proof: Proof. Proof using Hah Hal Hsa Hsl Hsh. unfold main_init. apply subcode_sss_compute_trans with (2 := empty_stack_spec s _ _); auto. apply subcode_sss_compute_trans with (2 := empty_stack_spec a _ _); auto. apply subcode_sss_compute_trans with (2 := empty_stack_spec h (6+i) _); auto. apply subcode_sss_compute_trans with (2 := empty_stack_spec l (9+i) _); auto. bsm sss PUSH with s Zero. bsm sss stop. f_equal. apply vec_pos_ext; intros x. dest x a; dest x l; dest x h; dest x s. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)