proposition: Lemma interpretP {M: ssm} {X Y: config} {φ ψ0 ψ1: valuation} : Forall (models φ ψ0 ψ1) (SM_to_SUcs M) -> reachable M X Y -> interpret φ ψ0 ψ1 X = interpret φ ψ0 ψ1 Y.
proof: Proof. move=> HM. elim; [| done | by move=> > ? ->]. move=> {}X {}Y [|] x y a b A B. - move: HM. rewrite /SM_to_SUcs Forall_map Forall_forall => HM. move /HM. rewrite /models /interpret. case: (φ (embed ([], [], y))); first done. move: a b => [|] [|] ? ? -> /=; by rewrite ascend_arr. - move: HM. rewrite /SM_to_SUcs Forall_map Forall_forall => HM. move /HM. rewrite /models /interpret. case: (φ (embed ([], [], x))); first done. move: a b => [|] [|] ? ? -> /=; by rewrite ascend_arr. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.StackMachines(SSM) Undecidability.StackMachines.Util(CSSM_facts) Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool