proposition: Lemma bounded_stack_difference {n: nat} {x y: state} {A B C D: stack} : bounded M n -> reachable M (A, B, x) (C, D, y) -> length B <= length D + n /\ length D <= length B + n.
proof: Proof. move /(_ (A, B, x)) => [L [HL1 HL2]]. move /reachable_to_reachable_n => [m]. have: forall Z : config, reachable_n m (A, B, x) Z -> In Z L. { move=> *. apply: HL1. apply: reachable_n_to_reachable. by eassumption. } move /(reachable_n_bounded (L := L)) /[apply]. move /reachable_n_monotone => /(_ n ltac:(lia)). clear m HL1 HL2 L. elim: n x y A B C D. { move=> > /reachable_0E [] *. subst. by lia. } move=> n IH x y A B C D /reachable_SnE. case. { move=> [] *. subst. by lia. } move=> [[[C' D'] z]] [/IH] {}IH. move HZ: (C', D', z) => Z. move HY: (C, D, y) => Y HZY. case: HZY HZ HY. - move=> > _ [] ? ? ? [] ? ? ?. subst. move: IH. rewrite /length -?/(length _). by lia. - move=> > _ [] ? ? ? [] ? ? ?. subst. move: IH. rewrite /length -?/(length _). by lia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM