proposition: Lemma log_terminates : f_terminates log_iter.
proof: Proof. intro. Subterm.rec_wf_rel IH x lt. destruct x. exists 0. exists 0. intros. inversion H. simpl. reflexivity. simpl. reflexivity. destruct x. exists 0. exists 0. intros. inversion H; simpl; reflexivity. specialize (IH (div2 (S (S x)))). forward IH. simpl. auto using div2_le with arith. destruct IH as [y Hy]. exists (S y). destruct Hy as [p Hp]. exists (S p). intros. destruct k. inversion H. simpl. rewrite Hp. auto. auto with arith. Defined.
imports: Equations(Equations) List Program.Syntax Arith Lia