proposition: Lemma solving_step {v w P n} : solving v w P (S n) -> adequate v w P n \/ solving v w P n \/ MPCPb ((v, w), P).
proof: Proof. move=> [A [HA [ξ /derE]]]. move=> [ζ [s [k]]]. rewrite {1}/Γ /In -/(In _ _). case. case; last case. { move=> ?. subst s. case: k. { move=> /= [_]. case=> _ _ _ -> /unify_words HA2 _ _ _. right. right. eexists. by constructor; eassumption. } move=> k /= [/Forall_cons_iff] [? _] *. left. eexists. eexists. by eassumption. } { move=> ?. subst s. case: k. { move=> /= [_]. case=> <- _ /(f_equal size) /=. by lia. } move=> k /= [/Forall_cons_iff] [? _] *. right. left. exists []. constructor; first done. eexists. move=> /=. rewrite ? app_nil_r. by eassumption. } { move /in_map_iff => [[x y]]. move=> [<- ?] /=. case: k; last case. - move=> [_] /=. case=> -> _ /(f_equal size) /=. by lia. - move=> /= [/Forall_cons_iff] [H1 _] [] H2. move: H1. rewrite H2. rewrite - ? /(substitute ζ (var _)). move=> + _ _ /(substitute_combine H2 (x := x)) Hx. move=> + /(substitute_combine H2 (x := y)) Hy _ _ _. rewrite Hx Hy => HD. right. left. exists (A ++ [(x, y)]). constructor. { apply: incl_app; first done. by apply /incl_cons. } exists ξ => /=. by rewrite tau1_lastP tau2_lastP ? app_assoc. - move=> k /= [/Forall_cons_iff] [_ /Forall_cons_iff] [? _] *. left. eexists. eexists. by eassumption. } Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP