proposition: Lemma DWK_H10 E: SOU X 3 (H10_to_DWK X E) -> H10 E.
proof: Proof. rewrite SOU_NSOU; eauto. intros (Delta & tau & T & EQ & N). exists (sub_sol tau). assert (forall e, e ∈ Eqs E -> tau • fst e ≡ tau • snd e) as H by now intros []; eauto. intros e Hin. destruct e; econstructor. all: edestruct (@in_Equations X (varEQ x) E) as [_ EQx]; mp EQx; [eexists; intuition eauto; cbn; intuition | eapply H in EQx]. 2, 3: edestruct (@in_Equations X (varEQ y) E) as [_ EQy]; mp EQy; [eexists; intuition eauto; cbn; intuition| eapply H in EQy]. 2, 3: edestruct (@in_Equations X (varEQ z) E) as [_ EQz]; mp EQz; [eexists; intuition eauto; cbn; intuition| eapply H in EQz]. all: eapply backward_vars in EQx as [n]; eauto. 2 - 3: eapply backward_vars in EQy as [m]; eauto. 2 - 3: eapply backward_vars in EQz as [p]; eauto. all: repeat (erewrite sub_sol_enc; [|eauto]). - eapply backward_consts; [eauto|]. eapply H, in_Equations; eexists; intuition eauto. cbn; intuition. - eapply backward_add; [eauto..|]. eapply H, in_Equations; eexists; intuition eauto. cbn; intuition. - eapply backward_mult; [eauto..|]. eapply H, in_Equations; eexists; intuition eauto. cbn; intuition. Qed.
imports: List Arith Lia Undecidability.HOU(std.std calculus.calculus) Undecidability.HOU.second_order(diophantine_equations dowek.encoding) Undecidability.HOU.unification.nth_order_unification