proposition: Lemma chain_proves a b c d n (f:chain n) : h10upc_sem_direct ((a,b),(c,d)) -> a < n -> b < n -> c < n -> d < n -> ierel (f a) (f b) (f c) (f d).
proof: Proof. Proof using HA3. rewrite h10_equiv. intros k; remember k as Habcd eqn:Heq; clear Heq; revert k. induction 1 as [a|a b c d b' c' d' H1 IH1 H2 IH2 H3 IH3 H4 IH4]; intros Ha Hb Hc Hd. - apply chain_succ. easy. - cbn -[erel] in HA3. specialize (@HA3 (f c) (f b) (f d) (f d') (f c') (f b') (f a)). rewrite !ierel_spec' in HA3. cbn in HA3. rewrite !chain_zero in *. assert (0 < n) as H0n by lia. assert (b' < n) as Hbn by (inversion H3; [lia | h10ind_not_lt_0]). assert (c' < n) as Hcn by (inversion H4; [lia | h10ind_not_lt_0]). assert (d' < n) as Hdn by (rewrite <- h10_equiv in H2; cbn in H2; lia). apply HA3; eauto. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Synthetic.Definitions