proposition: Lemma state_flip {s t X c b} : In ((s, t, X), c, b) M -> match X with | ('#? _) | ('#- _) | ('$? _) | ('+|) => b = false | _ => b = true end.
proof: Proof. rewrite /M ?in_app_iff -?lock. move=> [|[|[|]]]. - rewrite /index_ops ?in_app_iff ?in_map_iff. by move=> [|[|[|]]] [[? [? ?]]] [[]] *; subst. - rewrite /increase_ops ?in_app_iff ?in_map_iff. by move=> [|[|[|]]] [[? [? ?]]] [[]] *; subst. - rewrite /goto_ops ?in_app_iff in_flat_map. move=> [| [?] [_]]; rewrite in_map_iff; move=> [[? [[? ?] ?]]] [[]] *; by subst. - case /in_app_iff. + move=> /in_map_iff [[? [[? ?] ?]]] [[]] *. by subst. + case; [| case; [| case; [|done]]]; move=> [] *; by subst. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun