proposition: Lemma transl_size : forall (t : Term), size (transl t) <= 3 ^ (size t).
proof: Proof. induction t; sauto; try omega. assert (size (transl t1) + size (transl t2) <= 3 ^ size t1 + 3 ^ size t2). Reconstr.reasy (@Coq.Arith.PeanoNat.Nat.add_le_mono) Reconstr.Empty. assert (size (transl t1) + size (transl t2) + 1 <= 3 ^ size t1 + 3 ^ size t2 + 1). auto with zarith. Reconstr.reasy (@Coq.Arith.PeanoNat.Nat.le_lt_trans, @lem_pow_3, @Coq.Arith.PeanoNat.Nat.lt_succ_r) Reconstr.Empty. assert (size (abstr n (transl t)) <= 3 * size (transl t)). pose proof abstr_size; eauto with zarith. assert (size (abstr n (transl t)) <= 3 * 3 ^ size t). pose proof le_trans; eauto with zarith. assert (forall x : nat, 3 * 3 ^ x = 3 ^ (x + 1)). Reconstr.reasy (@Coq.Arith.PeanoNat.Nat.add_0_r, @Coq.Arith.PeanoNat.Nat.pow_succ_r', @Coq.Arith.PeanoNat.Nat.shiftl_1_l, @Coq.Arith.PeanoNat.Nat.pow_1_r, @Coq.Arith.PeanoNat.Nat.pow_0_r, @Coq.Arith.PeanoNat.Nat.add_succ_r) Reconstr.Empty. ycrush. Qed.
imports: Hammer(Reconstr) PeanoNat Omega