proposition: Theorem minimize_weight (M: SMN) : confluent M -> length_preserving M -> { M' : SMN | weight M' = 0 /\ (confluent M' /\ length_preserving M' /\ ((exists NM, bounded M NM) <-> (exists NM', bounded M' NM'))) }.
proof: Proof. elim /(Nat.measure_induction _ weight): M => M IH confluent_M lp_M. have [? |] : {weight M = 0} + {weight M <> 0} by decide equality. { exists M. by firstorder done. } move /overweight_Instruction => [[[[l r] x] [[l' r'] y]] []]. move: l => [|a l]; first last. { move /minimize_weight_lhs => H /H => /(_ confluent_M lp_M) => [[M' [? [? [? ?]]]]]. case: (IH M'); [ done | done | done |]. move=> M'' [? [? [? HM'']]]. exists M''. constructor; [done | constructor; [ done | constructor; [done | by rewrite -HM'']]]. } move: l' => [|a l']; first last. { move /minimize_weight_rhs => H /H => /(_ confluent_M lp_M) => [[M' [? [? [? ?]]]]]. case: (IH M'); [ done | done | done |]. move=> M'' [? [? [? HM'']]]. exists M''. constructor; [done | constructor; [ done | constructor; [done | by rewrite -HM'']]]. } move: r => [|a r]; first by (move /lp_M => /=; lia). move: r' => [|b r']; first by (move /lp_M => /=; lia). move: r => [|a' r]. - move: r' => [|? ?]; last by (move /lp_M => /=; lia). move=> + _ => /minimize_weight_short => /(_ confluent_M lp_M) => [[M' [? [? [? ?]]]]]. case: (IH M'); [ done | done | done |]. move=> M'' [? [? [? HM'']]]. exists M''. constructor; [done | constructor; [ done | constructor; [done | by rewrite -HM'']]]. - have : 1 <= length (a' :: r) by (move=> /=; lia). move: (a' :: r) => {}r. move /minimize_weight_length => H /H => {}H /H => /(_ confluent_M lp_M) => [[M' [? [? [? ?]]]]]. case: (IH M'); [ done | done | done |]. move=> M'' [? [? [? HM'']]]. exists M''. constructor; [done | constructor; [ done | constructor; [done | by rewrite -HM'']]]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun