proposition: Lemma minimize_weight_short {M: SMN} {a b x y} : In (([], [a], x), ([], [b], y)) M -> 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 confluent_M lp_M. pose z := fresh_State M. pose M1 := AddFreshLoop.M' M [] [a] [a] [] x z. pose M2 := DerivableRule.M' M1 [a] [] [] [b] z y. have : In ([], [a], x, ([], [b], 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] [] [b] x y. pose M4 := DerivableRule.M' (M21 ++ M22) [] [a] [] [b] 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 ([a], [], z) ([], [b], 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], x) ([], [b], y). { apply: (rt_trans (y := ([a], [], z))); apply: rt_step; (apply: (@DerivableRule.step_neq _ [] [a] [] [b] x y); first by [left | right]); apply /Reordering.simulation_step; rewrite /Reordering.M -HM2 /M2. - apply: (stepI [] [] [] [a] [a] [] x z); [done | done | clear; by firstorder done]. - apply: (stepI [] [] [a] [] [] [b] z y); [done | done | clear; by firstorder done]. } exists (M21 ++ M22). constructor; [| constructor; [| constructor]]. - suff: weight M2 < weight M + (weight_Instruction ([], [a], x, ([], [b], y))). { rewrite HM2 weight_split. move: (weight_Instruction _) (weight _). by lia. } rewrite /weight_Instruction /basic. rewrite /M2 /DerivableRule.M' /= /weight_Instruction /=. 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 | move=> /=; by lia | ]. apply /Reordering.length_preservation. rewrite /Reordering.M -HM2. apply /DerivableRule.length_preservation; [by eassumption | move=> /=; by 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