proposition: Theorem main_loop_complete v w q : v#>s = Zero::nil -> v#>h = nil -> v#>l = nil -> v#>a = nil -> out_code q (i,main_loop) -> (i,main_loop) // (i,v) ->> (q,w) -> p = q /\ (forall x, x <> s -> x <> a -> x <> h -> x <> l -> v#>x = w#>x) /\ tiles_solvable lt.
proof: Proof. Proof using Hp Hsh Hsa Hhl Hal Hah Hsl. intros H1 H2 H3 H4 H5 H6. rewrite <- (C2_eq _ H1); auto. destruct main_loop_complete_rec with (2 := H5) (3 := H6) as (G1 & k & G2 & G3). red; auto. split; auto. split; [ | exists k ]; auto. red in G3. intros; rewrite <- G3; 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)