proposition: Lemma transl_size : forall (t : Term), size (transl t) <= 3 ^ (size t).
proof: Proof. induction t; sintuition. - assert (size (transl t1) + size (transl t2) <= 3 ^ size t1 + 3 ^ size t2). { eauto using PeanoNat.Nat.add_le_mono. } assert (size (transl t1) + size (transl t2) + 1 <= 3 ^ size t1 + 3 ^ size t2 + 1). { auto with zarith. } hauto use: Nat.le_trans, lem_pow_3. - assert (size (abstr n (transl t)) <= 3 * size (transl t)). { eauto using abstr_size with zarith. } assert (size (abstr n (transl t)) <= 3 * 3 ^ size t). { eauto using Nat.le_trans with zarith. } assert (forall x : nat, 3 * 3 ^ x = 3 ^ (x + 1)) by hauto using Nat.add_1_r. congruence. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz