proposition: Theorem construct_basic_SMN (M: SMN) : confluent M -> length_preserving M -> { M' : SMN | Forall basic M' /\ (confluent M' /\ ((exists NM, bounded M NM) <-> (exists NM', bounded M' NM'))) }.
proof: Proof. move /Transform.minimize_weight => H /H => [[M']] [HM'] [? [_ ?]]. exists M'. constructor; last by constructor. apply /Forall_forall => op /(@in_split Instruction) => [[?]] [? ?]. subst M'. move: HM'. rewrite Transform.weight_split => ?. have : Transform.weight_Instruction op = 0 by lia. clear. rewrite /Transform.weight_Instruction. case Hop: (Transform.basic op); last by move: op Hop => [[[l r] ?] [[l' r'] ?]]. move: op Hop => [[[l r] ?] [[l' r'] ?]] /=. move: l r l' r' => [|a [|? ?]] [|b [|? ?]] [|a' [|? ?]] [|b' [|? ?]] *; by [| apply: basic_r | apply: basic_l]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun