proposition: Fact tile_spec i v st : st = (length tile+i,v[(high++v#>x)/x][(low++v#>y)/y]) -> (i,tile) // (i,v) ->> st.
proof: Proof. Proof using Hxy. intro; subst. unfold tile. apply sss_compute_trans with (st2 := (length (half_tile x (rev high))+i,v[(high++v#>x)/x])). rewrite <- (rev_involutive high) at 3. apply subcode_sss_compute with (P := (i,half_tile x (rev high))). subcode_tac. apply half_tile_spec. rewrite <- (rev_involutive low) at 3. apply subcode_sss_compute with (P := (length (half_tile x (rev high))+i,half_tile y (rev low))). subcode_tac; solve list eq. replace (length (half_tile x (rev high) ++ half_tile y (rev low)) + i) with (length (half_tile y (rev low)) + (length (half_tile x (rev high)) + i)). replace (v#>y) with (v[(high ++ v#>x)/x]#>y) by rew vec. apply half_tile_spec. rew length; lia. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)