proposition: Lemma construct_chain_at (h:nat) HH : (h>0) -> incl (F_succ_right :: F_succ_left :: F_zero :: nil) HH -> (forall c:chain h, (chain_exists c ++ HH) ⊢I wFalse 1) -> HH ⊢I wFalse 1.
proof: Proof. intros Hn HHH H. induction h as [|h IH]. - exfalso. lia. - destruct h as [|h]. + clear IH. apply (IE (phi:=(∀ (∀ (∀ P 2 3 3 (P 0 1 3 (Pr $2 $0 → wFalse (4)))))))). * eapply IE. 2: apply Ctx,HHH; do 2 right; now left. doAllE ($0) (N 0 → (∀ (∀ (∀ P 2 3 4 (P 0 1 4 (Pr $2 $0 → wFalse 5))))) → wFalse (2)). 1: easy. apply Ctx,HHH. right. now left. * doAllI pl. doAllI n1. doAllI pr. apply intros_P. cbn -[intros_defs]. apply II. eapply Weak. 1:apply (H (chainS n1 pl pr chainZ)). apply incl_app. 2: do 11 apply incl_tl; reflexivity. cbn -[map]. intros f [Hf|[Hf|[Hf|[Hf|[Hf|[Hf|[Hf|[Hf|[Hf|[]]]]]]]]]]; rewrite <- Hf; let rec find n := match n with 0 => now left | S ?nn => (now left) + (right; find nn) end in find 11. + apply IH; [lia|clear IH]. intros c. eapply (IE (phi:=(∀ (∀ (∀ P 2 (3+findNum c (S h)) 3 (P 0 1 3 (Pr $2 $0 → wFalse 4))))))). * unfold F_succ_left. unfold Not. eapply IE. 2: apply Ctx, in_or_app; left; eapply chain_proves_N; easy. doAllE ($(findNum c (S h))) (N 0 → (∀ (∀ (∀ P 2 3 4 (P 0 1 4 (Pr $2 $0 → wFalse 5))))) → wFalse 2). -- easy. -- apply Ctx. apply in_or_app. right. apply HHH. right. now left. * doAllI pl. doAllI nh. doAllI pr. apply intros_P. cbn -[intros_defs]. apply II. eapply Weak. 1:apply (H (chainS nh pl pr c)). apply incl_app. 2: do 11 apply incl_tl; now apply incl_appr. cbn -[map]. intros f [Hf|[Hf|[Hf|[Hf|[Hf|[Hf|[Hf|[Hf|H1]]]]]]]]. 9: do 11 right; apply in_or_app; now left. all: rewrite <- Hf; let rec find n := match n with 0 => now left | S ?nn => (now left) + (right; find nn) end in find 11. 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)