proposition: Lemma ζ_equivP {n: nat} {x x': state} {A B A' B': stack} : bounded' n -> equiv (A, B, x) (A', B', x') -> ζ (S n - length B) (A, B, x) = ζ (S n - length B') (A', B', x').
proof: Proof. Proof using confluent_M. move /(extend_bounded' confluent_M) => Hn. move Hm: (S n - length B)=> m. elim: m A B A' B' Hm. - move=> A B A' B' HnB Hxx'. have [-> | HnB']: (S n - length B' = 0 \/ S n - length B' = (S (n - length B'))) by lia. { rewrite ? ζ_0P. do 2 f_equal. by apply: nf_equiv_eq. } rewrite HnB' ζ_0P ζ_SnP. case: (narrow_dec (A', B', x')) => /=; first last. { move=> _. do 2 f_equal. by apply: nf_equiv_eq. } move /equiv_sym in Hxx'. move /(narrow_equiv confluent_M Hxx') /Hn => /=. by lia. - move=> m IH A B A' B' Hm Hxx'. have [HnB' | ->]: (S n - length B' = 0 \/ S n - length B' = S (n - length B')) by lia. { rewrite HnB' ζ_0P ζ_SnP. case: (narrow_dec (A, B, x)) => /=; first last. - move=> _. do 2 f_equal. by apply: nf_equiv_eq. - move /(narrow_equiv confluent_M Hxx') /Hn => /=. by lia. } rewrite ?ζ_SnP. case: (narrow_dec (A, B, x)); case: (narrow_dec (A', B', x'))=> /=. + move=> _ _. apply: (arr_eqI (s := fun=> ζ _ _) (t := fun=> ζ _ _)). move=> b. have -> : n - length B' = S n - length (B' ++ [b]) by (rewrite app_length /length; lia). apply: IH; [ rewrite app_length /length -/(length _); by lia | by apply: equiv_appR]. + by move=> + /(narrow_equiv confluent_M Hxx'). + by move=> /(narrow_equiv confluent_M ((iffLR equiv_sym) Hxx')). + move=> _ _. do 2 f_equal. by apply: nf_equiv_eq. 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