proposition: Lemma completeness {M: cssm}: SSemiU (SM_to_SUcs (proj1_sig M)) -> CSSM_UB M.
proof: Proof. case: M=> M confluent_M /=. move=> [φ [ψ0 [ψ1]]]. rewrite -Forall_forall => Hφ. pose f x := embed (([], [], x) : config). apply: (bounded_of_bounded' confluent_M (n := depth_bound φ (map f (enum_states M)))). move=> /= Z x y A B Hx Hy. case: (In_dec _ y (enum_states M)); first by decide equality. { move=> /(in_map f) /depth_boundP => /(_ φ) Hfy. move: Hy => /(interpretP Hφ). move: Hx => /(interpretP Hφ) <- /= /descendP. rewrite -/(f y). move: (length B) => ?. by lia. } move: (Hy) Hx => /enum_states_reachable [<- /enum_states_reachable | ]; last by by move=> [+]. case; last by move=> [+]. case=> *. subst=> /=. by lia. 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