proposition: Theorem G4_length : reachable (quad (3 * 2 ^ (3 * 2 ^ (3 ^3) + 3 ^3) - 1) 0 0 0).
proof: Proof. generalize big_number_eq. generalize (3 * 2 ^ (3 * 2 ^ 3 ^ 3 + 3 ^ 3) - 1). generalize Final. generalize (f (f 27 + 28)). induction 2. auto. Qed.
imports: Arith Omega Relations