proposition: Lemma ψζP {n: nat} {x: state} {A B: stack} {a: bool} : bounded' n -> ζ (S n - length B) (A ++ [a], B, x) = substitute (ψ a (S n)) (ζ (S n - length B) (A, B, x)).
proof: Proof. Proof using confluent_M. move=> Hn. move Hm: (S n - length B)=> m. elim: m x A B Hm. - move=> x A B Hm. rewrite ? ζ_0P /= ψP. move HAxB: (nf (A, B, x)) => [[A' B'] x']. have [-> | ?]: S n - length B' = 0 \/ S n - length B' > 0 by lia. { rewrite ζ_0P. f_equal. f_equal. apply: nf_equiv_eq. apply: equiv_appL. rewrite -HAxB. by apply: nf_equiv. } have Hxx': equiv (A' ++ [a], B', x') (A ++ [a], B, x). { apply: equiv_appL. rewrite equiv_sym -HAxB. by apply: nf_equiv. } by rewrite (ζ_equivP Hn Hxx') Hm ζ_0P. - move=> m IH x A B Hm. rewrite ? ζ_SnP. case: (narrow_dec (A, B, x)). + move=> /= /(narrow_appL (a := a)) => ?. case: (narrow_dec (A ++ [a], B, x)); last done. move=> _ /=. apply: (arr_eqI (s := fun => ζ _ _) (t := fun => substitute _ _)). move=> b. apply: IH. rewrite app_length /length -/(length _). by lia. + move=> _ /=. rewrite -(ζ_SnP (A := A ++ [a])). rewrite ψP. move HAxB: (nf (A, B, x)) => [[A' B'] x']. rewrite -Hm. have Hxx': equiv (A ++ [a], B, x) (A' ++ [a], B', x'). { apply: equiv_appL. rewrite -HAxB. by apply: nf_equiv. } by rewrite (ζ_equivP Hn Hxx'). 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