proposition: Lemma find_largest_variable p : { n | bounded_indi_term n (encode_polynomial p) }.
proof: Proof. induction p; cbn. - exists 0. now induction n. - exists (S n). lia. - destruct d; cbn. + destruct IHp1 as [n], IHp2 as [m]. destruct (Arith.Compare_dec.le_lt_dec n m). * exists m. repeat split. 2: easy. now apply (bounded_indi_term_up n m). * exists n. repeat split. easy. apply (bounded_indi_term_up m n). lia. easy. + destruct IHp1 as [n], IHp2 as [m]. destruct (Arith.Compare_dec.le_lt_dec n m). * exists m. repeat split. 2: easy. now apply (bounded_indi_term_up n m). * exists n. repeat split. easy. apply (bounded_indi_term_up m n). lia. easy. Qed.
imports: PeanoNat Lia Vector List Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts PA2_categoricity) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.H10(H10p) Undecidability.Shared.Dec