proposition: Lemma soundness {M: cssm} : CSSM_UB M -> SSemiU (SM_to_SUcs (proj1_sig M)).
proof: Proof. Opaque ζ ψ. case: M=> M confluent_M. rewrite /CSSM_UB /SSemiU. move /(boundedP confluent_M) => /= [n HnM]. exists (fun i => @ζ M (S n) (unembed i)), (@ψ M false (S n)), (@ψ M true (S n)). move=> [[a x]] => [[y b]] /=. move /SM_to_SUcsP => [x' [y' [-> [->]]]] /equiv_sym Hxy. rewrite ?embedP ζ_nilP (itebP (P := fun _ => ζ _ _)). have /= := ζ_equivP confluent_M HnM Hxy. have ->: n - 0 = n by lia. move=> ->. rewrite (itebP (P := fun=> ψ _ _)). by apply: (ψζP _ HnM (A := []) (B := [])). 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