proposition: Fact half_tile_spec i l v : (i,half_tile l) // (i,v) ->> (length (half_tile l)+i,v[(rev l++v#>x)/x]).
proof: Proof. rewrite half_tile_length. revert i v; induction l as [ | b l IHl ]; intros i v; simpl. bsm sss stop; f_equal. apply vec_pos_ext; intros z; dest z x. bsm sss PUSH with x b. specialize (IHl (1+i) (v[(b::v#>x)/x])). apply subcode_sss_compute with (P := (1+i,half_tile l)). subcode_tac; solve list eq. eq goal IHl; do 2 f_equal. lia. apply vec_pos_ext; intros z; dest z x. solve list eq. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)