proposition: Lemma F4 : reachable (quad (f 4) 1 (f 3) 0).
proof: Proof. rewrite (f_Sn 3). eapply reachable_Rgstar. eexact SF3. replace (S (2 * (f 3))) with (f 3 + (S ( f 3))). apply L2. compute. trivial. Qed.
imports: Arith Omega Relations