proposition: Lemma transport_prove : nil ⊢I F (h10:=h10).
proof: Proof. Proof using Hφ φ. unfold F. do 3 apply AllI. cbn. do 4 apply II. pose ((S (highest_var_list h10))) as h10vars. fold h10vars. pose (highest_num φ h10vars) as h10max. pose proof (@highest_num_descr φ h10vars) as Hvars. fold h10max in Hvars. eapply (@construct_chain_at (S h10max)). 1:lia. 1:now apply incl_tl. intros cc. epose proof (@emplace_forall_elim h10vars _ (fun k => findNum cc (φ k))) as Hpr. eapply IE. 2:eapply Hpr. 2: apply Ctx, in_or_app; right; now left. eapply Weak. 2: apply incl_app; [apply incl_appl;reflexivity|apply incl_appr,incl_tl;reflexivity]. apply II. clear Hpr. assert (h10vars >= S( highest_var_list h10)) as Hless. 1: lia. induction h10 as [|h h10' IHh] in Hvars,Hφ,Hless|-*. - apply Ctx. left. unfold translate_rec, wFalse, subst_form,Vector.map. do 3 f_equal. 1: change(S h10vars) with (1+h10vars). all: cbn [subst_term]; rewrite specialize_n_resolve; destruct Dec; lia + f_equal;lia. - cbn -[Nat.mul h10vars chain_exists subst_form]. apply II in IHh. 2: intros c' Hc; apply Hφ; now right. 2: exact Hvars. 2: cbn in Hless; lia. eapply IE. 1: eapply Weak. 1: exact IHh. 1: now apply incl_tl. eapply IE. 1: apply Ctx; left; now cbn [subst_form]. eapply Weak. 2: apply incl_tl; reflexivity. unfold translate_single. destruct h as [[a b][c d]]. rewrite erel_ereli. clear IHh. unfold Not. erewrite (@erel_i_subst _ _ _ _ _ _ (fun k : nat => if Dec (k < h10vars) then findNum cc (φ k) else ((k - h10vars)))). 3: repeat destruct Dec; (exfalso;lia) + lia. 2: intros n; rewrite specialize_n_resolve; destruct (Dec _); (exfalso;lia)+var_eq. destruct (highest_var_descr ((a,b),(c,d))) as [Hlessa [Hlessb [Hlessc Hlessd]]]. cbn in Hless. do 4 (destruct Dec as [htr|hff]; [clear htr|exfalso;lia]). do 1 (destruct Dec; [exfalso;lia|idtac]). assert (forall a,S a - a=1) as -> by (intros;lia). eapply Weak. 1: eapply (prove_single). + specialize (Hvars b ltac:(lia)). lia. + specialize (Hvars a ltac:(lia)). lia. + specialize (Hvars c ltac:(lia)). lia. + specialize (Hvars d ltac:(lia)). lia. + apply (@Hφ ((a,b),(c,d))). now left. + easy. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)