proposition: Lemma mortal_K_bound k p a b : mortal k (p, (Nat.min (S k) a, Nat.min (S k) b)) -> mortal k (p, (a, b)).
proof: Proof. move=> /mortal_steps_iff H. apply /mortal_steps_iff. have [/Nat.min_r <-|?] : a <= S k \/ S k < a by lia. - have [/Nat.min_r <-|?] : b <= S k \/ S k < b by lia. + done. + have ->: b = (Nat.min (S k) b) + (b - (S k)) by lia. rewrite shift_steps_b; [lia|]. by rewrite H. - have ->: a = (Nat.min (S k) a) + (a - (S k)) by lia. rewrite shift_steps_a; [lia|]. have [/Nat.min_r <-|?] : b <= S k \/ S k < b by lia. + by rewrite H. + have ->: b = (Nat.min (S k) b) + (b - (S k)) by lia. rewrite shift_steps_b; [lia|]. by rewrite H. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties ConstructiveEpsilon Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Deciders.MM2_UBOUNDED_dec Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun