proposition: Lemma minimize_weight_lhs {M: SMN} {a l r l' r' x y} : In (a :: l, r, x, (l', r', y)) M -> weight_Instruction (a :: l, r, x, (l', r', y)) <> 0 -> confluent M -> length_preserving M -> { M' : SMN | weight M' < weight M /\ (confluent M' /\ length_preserving M' /\ ((exists NM, bounded M NM) <-> (exists NM', bounded M' NM'))) }.
proof: Proof. move=> HM Hop confluent_M lp_M. pose z := fresh_State M. pose M1 := AddFreshLoop.M' M [a] [] [] [a] x z. pose M2 := DerivableRule.M' M1 l (a::r) l' r' z y. have : In (a :: l, r, x, (l', r', y)) M2. { rewrite /M2 /M1 /AddFreshLoop.M' /DerivableRule.M' ?in_app_iff. move: HM. clear. by firstorder done. } move /in_split_informative => /(_ ltac:(by do 5 (decide equality))) => [[[M21 M22] HM2]]. pose M3 := Reordering.M' M21 M22 (a :: l) r l' r' x y. pose M4 := DerivableRule.M' (M21 ++ M22) (a::l) r l' r' x y. have ? : x <> z by (move: HM => /fresh_StateP; subst z; lia). have ? : y <> z by (move: HM => /fresh_StateP; subst z; lia). have ? : reachable M1 (l, a :: r, z) (l', r', y). { apply: AddFreshLoop.step_fresh_rI; first by (move=> /=; lia). apply: rt_step. move: HM => /transition => /(_ [] []). by rewrite ?app_norm. } have ? : reachable (M21 ++ M22) (a :: l, r, x) (l', r', y). { apply: (rt_trans (y := (l, a :: r, z))); apply: rt_step; (apply: (@DerivableRule.step_neq _ (a :: l) r l' r' x y); first by [left | right]); apply /Reordering.simulation_step; rewrite /Reordering.M -HM2 /M2. - apply: (stepI l r [a] [] [] [a] x z); [done | done | clear; by firstorder done ]. - apply: (stepI [] [] l (a :: r) l' r' z y); [by rewrite ?app_norm | by rewrite ?app_norm | clear; by firstorder done ]. } exists (M21 ++ M22). constructor; [| constructor; [| constructor]]. - suff: weight M2 < weight M + (weight_Instruction (a :: l, r, x, (l', r', y))). { rewrite HM2 weight_split. move: (weight_Instruction _) (weight _). by lia. } move: Hop. rewrite /M2 /DerivableRule.M' /= /weight_Instruction. case: (basic (a :: l, r, x, (l', r', y))); first by lia. move=> _. case: (basic (l, a :: r, z, (l', r', y))). { rewrite /= ?app_length. by lia. } rewrite /= ?app_length /= ?app_length. by lia. - apply /DerivableRule.confluence; first by eassumption. apply /Reordering.confluence. rewrite /Reordering.M -HM2. apply /DerivableRule.confluence; first by eassumption. apply: AddFreshLoop.confluent_M'; [done | done | by apply: fresh_StateP' | by move=> /=; lia ]. - apply /DerivableRule.length_preservation; [by eassumption | rewrite app_length /=; lia | ]. apply /Reordering.length_preservation. rewrite /Reordering.M -HM2. apply /DerivableRule.length_preservation; [by eassumption | rewrite app_length /=; lia | ]. apply: AddFreshLoop.length_preserving_M'; [done | done | by apply: fresh_StateP' | by move=> /=; lia ]. - rewrite (DerivableRule.boundedness (M21 ++ M22)); first by eassumption. rewrite -(Reordering.boundedness M21 M22). rewrite /Reordering.M -HM2. rewrite -(DerivableRule.boundedness); first by eassumption. rewrite -(AddFreshLoop.boundedness); [done | by apply: fresh_StateP' | by move=> /=; lia | done ]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun