proposition: Theorem main_loop_sound v : v#>s = Zero::nil -> v#>h = nil -> v#>l = nil -> v#>a = nil -> tiles_solvable lt -> exists w, (i,main_loop) // (i,v) ->> (p,w) /\ forall x, x <> s -> x <> a -> x <> h -> x <> l -> v#>x = w#>x.
proof: Proof. Proof using Hsh Hsa Hhl Hal Hah Hsl. intros H1 H2 H3 H4. rewrite <- (C2_eq _ H1); auto. intros H5. destruct main_loop_sound_rec with (2 := H5) as (k & w & Hw1 & Hw2). red; auto. exists w; split; auto. unfold spec in Hw2 |- *. intros; rewrite <- Hw2; auto. rewrite iter_f_v; rew vec. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)