Euler's theorem for units — exact evidence

Current Alpha v34 checked use; first admitted v31; not Stable. Original HA and the independently compiled Lean checker have freshly verified the complete bundle before this page was generated.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

210 checked bundle nodes · 568 proof edges · 12452 body proof nodes.

Literal self-contained proof bundle · SHA-256 1edfcb7021a0869c2493383c75dea367d757be0b77f36fc6ad3f5fd18ed38210

euler_units_candidate.py · euler_units_product_candidate.py · euler_units_residue_candidate.py

Unchanged historical local checkpoint record · Historical snapshot manifest. Those records retain their original non-admitting flags; current authority comes from the separate freshly verified v31 release.

Exact theorem nodes and inherited prerequisites

EU0001 euler_coprime_mod_transport · actual bundle node 177
EU0002 euler_multiplier_coprime_iff · actual bundle node 178
EU0004 euler_modular_unit_coprime · actual bundle node 179
EU0005 euler_coprime_modular_unit · actual bundle node 180
EU0006 euler_multiplier_residue_exists · actual bundle node 181
EU0007 euler_multiplier_prefix_empty · actual bundle node 182
EU0008 euler_multiplier_prefix_extend · actual bundle node 183
EU0009 euler_multiplier_prefix_exists · actual bundle node 184
EU000A euler_multiplier_prefix_entry · actual bundle node 185
EU000B euler_multiplier_prefix_bounded_injective · actual bundle node 186
EU000C euler_multiplier_prefix_permutation · actual bundle node 187
EU000D euler_multiplier_permutation_exists · actual bundle node 188
EU000E euler_unit_product_factor_exists · actual bundle node 189
EU000F euler_unit_product_factor_unit_value · actual bundle node 190
EU0010 euler_unit_product_factor_nonunit_value · actual bundle node 191
EU0011 euler_unit_product_factor_coprime · actual bundle node 192
EU0012 euler_unit_product_prefix_empty · actual bundle node 193
EU0013 euler_unit_product_prefix_extend · actual bundle node 194
EU0014 euler_unit_product_prefix_exists · actual bundle node 195
EU0015 euler_unit_product_prefix_drop_last · actual bundle node 196
EU0016 euler_unit_product_prefix_entry · actual bundle node 197
EU0017 euler_unit_product_coprime · actual bundle node 198
EU0018 euler_unit_factor_scaled_congruence · actual bundle node 199
EU0019 euler_nonunit_factor_unchanged_congruence · actual bundle node 200
EU001A euler_unit_scaled_prefix_drop_last · actual bundle node 201
EU001B euler_unit_product_reindex_scale · actual bundle node 202
EU001D euler_coprime_weighted_product_cancel · actual bundle node 203
EU001E euler_unit_count_product_balance · actual bundle node 204
EU001F euler_coprime_totient_power_value · actual bundle node 205
EU0020 euler_coprime_totient_power · actual bundle node 206
EU0021 euler_modular_unit_totient_power · actual bundle node 207
EU0022 euler_theorem_for_units · actual bundle node 208
add_comm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m. n + m = m + n
```

beta_at_unique · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c i x y. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y) -> x = y

beta_prefix_extend · checked inherited prerequisite

Exact statement in the checked dependency cone

forall k b e s. exists z c. (((exists h. h + S s = S ((S k) * c)) /\ exists q. z = q * S ((S k) * c) + s) /\ forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. z = q * S ((S i) * c) + a))

beta_product_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c l. exists n u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S (S i)) * v)) /\ exists q. u = q * S ((S (S i)) * v) + s) /\ s = r * p)))))

beta_product_permutation_invariant · checked inherited prerequisite

Exact statement in the checked dependency cone

forall l r s b c z d p q. (forall fp_i_reindex_bounded. (exists fp_gap_reindex_bounded_index. fp_gap_reindex_bounded_index + S fp_i_reindex_bounded = l) -> exists fp_value_reindex_bounded. ((((exists ff_h_reindex_bounded_entry. ff_h_reindex_bounded_entry + S (fp_value_reindex_bounded) = S ((S (fp_i_reindex_bounded)) * s)) /\ exists ff_q_reindex_bounded_entry. r = ff_q_reindex_bounded_entry * S ((S (fp_i_reindex_bounded)) * s) + (fp_value_reindex_bounded))) /\ (exists fp_gap_reindex_bounded_value. fp_gap_reindex_bounded_value + S fp_value_reindex_bounded = l))) -> (forall fp_i_reindex_injective fp_j_reindex_injective fp_value_reindex_injective. (exists fp_gap_reindex_injective_i. fp_gap_reindex_injective_i + S fp_i_reindex_injective = l) -> (exists fp_gap_reindex_injective_j. fp_gap_reindex_injective_j + S fp_j_reindex_injective = l) -> (((exists ff_h_reindex_injective_left. ff_h_reindex_injective_left + S (fp_value_reindex_injective) = S ((S (fp_i_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_left. r = ff_q_reindex_injective_left * S ((S (fp_i_reindex_injective)) * s) + (fp_value_reindex_injective))) -> (((exists ff_h_reindex_injective_right. ff_h_reindex_injective_right + S (fp_value_reindex_injective) = S ((S (fp_j_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_right. r = ff_q_reindex_injective_right * S ((S (fp_j_reindex_injective)) * s) + (fp_value_reindex_injective))) -> fp_i_reindex_injective = fp_j_reindex_injective) -> (forall fpr_i_reindex_aligned fpr_j_reindex_aligned fpr_x_reindex_aligned. (exists fpr_h_reindex_aligned. fpr_h_reindex_aligned + S fpr_i_reindex_aligned = l) -> (((exists ff_h_reindex_aligned_map. ff_h_reindex_aligned_map + S (fpr_j_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * s)) /\ exists ff_q_reindex_aligned_map. r = ff_q_reindex_aligned_map * S ((S (fpr_i_reindex_aligned)) * s) + (fpr_j_reindex_aligned))) -> (((exists ff_h_reindex_aligned_source. ff_h_reindex_aligned_source + S (fpr_x_reindex_aligned) = S ((S (fpr_j_reindex_aligned)) * c)) /\ exists ff_q_reindex_aligned_source. b = ff_q_reindex_aligned_source * S ((S (fpr_j_reindex_aligned)) * c) + (fpr_x_reindex_aligned))) -> (((exists ff_h_reindex_aligned_target. ff_h_reindex_aligned_target + S (fpr_x_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * d)) /\ exists ff_q_reindex_aligned_target. z = ff_q_reindex_aligned_target * S ((S (fpr_i_reindex_aligned)) * d) + (fpr_x_reindex_aligned)))) -> (exists ff_u_reindex_source_product ff_v_reindex_source_product. ((((exists ff_h_reindex_source_product_start. ff_h_reindex_source_product_start + S (1) = S ((S (0)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_start. ff_u_reindex_source_product = ff_q_reindex_source_product_start * S ((S (0)) * ff_v_reindex_source_product) + (1))) /\ ((((exists ff_h_reindex_source_product_terminal. ff_h_reindex_source_product_terminal + S (p) = S ((S (l)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_terminal. ff_u_reindex_source_product = ff_q_reindex_source_product_terminal * S ((S (l)) * ff_v_reindex_source_product) + (p))) /\ forall ff_i_reindex_source_product. (exists ff_lt_reindex_source_product_bound. ff_lt_reindex_source_product_bound + S ff_i_reindex_source_product = l) -> exists ff_p_reindex_source_product ff_r_reindex_source_product ff_s_reindex_source_product. ((((exists ff_h_reindex_source_product_factor. ff_h_reindex_source_product_factor + S (ff_p_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * c)) /\ exists ff_q_reindex_source_product_factor. b = ff_q_reindex_source_product_factor * S ((S (ff_i_reindex_source_product)) * c) + (ff_p_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_partial. ff_h_reindex_source_product_partial + S (ff_r_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_partial. ff_u_reindex_source_product = ff_q_reindex_source_product_partial * S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_r_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_successor. ff_h_reindex_source_product_successor + S (ff_s_reindex_source_product) = S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_successor. ff_u_reindex_source_product = ff_q_reindex_source_product_successor * S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_s_reindex_source_product))) /\ ff_s_reindex_source_product = ff_r_reindex_source_product * ff_p_reindex_source_product)))))) -> (exists ff_u_reindex_target_product ff_v_reindex_target_product. ((((exists ff_h_reindex_target_product_start. ff_h_reindex_target_product_start + S (1) = S ((S (0)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_start. ff_u_reindex_target_product = ff_q_reindex_target_product_start * S ((S (0)) * ff_v_reindex_target_product) + (1))) /\ ((((exists ff_h_reindex_target_product_terminal. ff_h_reindex_target_product_terminal + S (q) = S ((S (l)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_terminal. ff_u_reindex_target_product = ff_q_reindex_target_product_terminal * S ((S (l)) * ff_v_reindex_target_product) + (q))) /\ forall ff_i_reindex_target_product. (exists ff_lt_reindex_target_product_bound. ff_lt_reindex_target_product_bound + S ff_i_reindex_target_product = l) -> exists ff_p_reindex_target_product ff_r_reindex_target_product ff_s_reindex_target_product. ((((exists ff_h_reindex_target_product_factor. ff_h_reindex_target_product_factor + S (ff_p_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * d)) /\ exists ff_q_reindex_target_product_factor. z = ff_q_reindex_target_product_factor * S ((S (ff_i_reindex_target_product)) * d) + (ff_p_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_partial. ff_h_reindex_target_product_partial + S (ff_r_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_partial. ff_u_reindex_target_product = ff_q_reindex_target_product_partial * S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_r_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_successor. ff_h_reindex_target_product_successor + S (ff_s_reindex_target_product) = S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_successor. ff_u_reindex_target_product = ff_q_reindex_target_product_successor * S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_s_reindex_target_product))) /\ ff_s_reindex_target_product = ff_r_reindex_target_product * ff_p_reindex_target_product)))))) -> p = q

beta_product_succ_decompose · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c l n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + n) /\ forall i. (exists h. h + S i = S l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> exists p r. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ ((exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) /\ n = r * p))

beta_product_zero · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + n) /\ forall i. (exists h. h + S i = 0) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> n = 1

binary_modulus_nontrivial_nonzero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m. (exists ff_modulus_gap_binary_guard. ff_modulus_gap_binary_guard + S 1 = m) -> ~(m = 0)
```

coprime_bounded_mod_inverse · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a m. ~(m = 0) -> (forall hmi_divisor_assumption. (exists hmi_left_factor_assumption. a = hmi_divisor_assumption * hmi_left_factor_assumption) -> (exists hmi_right_factor_assumption. m = hmi_divisor_assumption * hmi_right_factor_assumption) -> hmi_divisor_assumption = 1) -> exists r. (exists hmi_gap_result_bound. hmi_gap_result_bound + S r = m) /\ (exists hmi_left_offset_result_inverse hmi_right_offset_result_inverse. a * r + m * hmi_left_offset_result_inverse = 1 + m * hmi_right_offset_result_inverse)

coprime_mul_left · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a b n. (forall d. (exists x. a = d * x) -> (exists y. n = d * y) -> d = 1) -> (forall d. (exists x. b = d * x) -> (exists y. n = d * y) -> d = 1) -> forall d. (exists x. a * b = d * x) -> (exists y. n = d * y) -> d = 1

coprime_one_left · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a d. (exists x. 1 = d * x) -> (exists y. a = d * y) -> d = 1
```
division_remainder_exists · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m n. ~(m = 0) -> exists q r. n = m * q + r /\ S r <= m
```

finite_beta_composition_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall r s b c l. exists z d. (forall fms_i_compose fms_j_compose fms_v_compose. (exists fms_gap_compose. fms_gap_compose + S (fms_i_compose) = (l)) -> (((exists fs_h_fms_compose_index. fs_h_fms_compose_index + S (fms_j_compose) = S ((S (fms_i_compose)) * s)) /\ exists fs_q_fms_compose_index. r = fs_q_fms_compose_index * S ((S (fms_i_compose)) * s) + (fms_j_compose))) -> (((exists fs_h_fms_compose_source. fs_h_fms_compose_source + S (fms_v_compose) = S ((S (fms_j_compose)) * c)) /\ exists fs_q_fms_compose_source. b = fs_q_fms_compose_source * S ((S (fms_j_compose)) * c) + (fms_v_compose))) -> (((exists fs_h_fms_compose_target. fs_h_fms_compose_target + S (fms_v_compose) = S ((S (fms_i_compose)) * d)) /\ exists fs_q_fms_compose_target. z = fs_q_fms_compose_target * S ((S (fms_i_compose)) * d) + (fms_v_compose))))

finite_bounded_injective_surjective · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n b c. (forall fp_i_pigeon_bounded. (exists fp_gap_pigeon_bounded_index. fp_gap_pigeon_bounded_index + S fp_i_pigeon_bounded = n) -> exists fp_value_pigeon_bounded. ((((exists ff_h_pigeon_bounded_entry. ff_h_pigeon_bounded_entry + S (fp_value_pigeon_bounded) = S ((S (fp_i_pigeon_bounded)) * c)) /\ exists ff_q_pigeon_bounded_entry. b = ff_q_pigeon_bounded_entry * S ((S (fp_i_pigeon_bounded)) * c) + (fp_value_pigeon_bounded))) /\ (exists fp_gap_pigeon_bounded_value. fp_gap_pigeon_bounded_value + S fp_value_pigeon_bounded = n))) -> (forall fp_i_pigeon_injective fp_j_pigeon_injective fp_value_pigeon_injective. (exists fp_gap_pigeon_injective_i. fp_gap_pigeon_injective_i + S fp_i_pigeon_injective = n) -> (exists fp_gap_pigeon_injective_j. fp_gap_pigeon_injective_j + S fp_j_pigeon_injective = n) -> (((exists ff_h_pigeon_injective_left. ff_h_pigeon_injective_left + S (fp_value_pigeon_injective) = S ((S (fp_i_pigeon_injective)) * c)) /\ exists ff_q_pigeon_injective_left. b = ff_q_pigeon_injective_left * S ((S (fp_i_pigeon_injective)) * c) + (fp_value_pigeon_injective))) -> (((exists ff_h_pigeon_injective_right. ff_h_pigeon_injective_right + S (fp_value_pigeon_injective) = S ((S (fp_j_pigeon_injective)) * c)) /\ exists ff_q_pigeon_injective_right. b = ff_q_pigeon_injective_right * S ((S (fp_j_pigeon_injective)) * c) + (fp_value_pigeon_injective))) -> fp_i_pigeon_injective = fp_j_pigeon_injective) -> (forall fp_value_pigeon_surjective. (exists fp_gap_pigeon_surjective_value. fp_gap_pigeon_surjective_value + S fp_value_pigeon_surjective = n) -> exists fp_i_pigeon_surjective. ((exists fp_gap_pigeon_surjective_index. fp_gap_pigeon_surjective_index + S fp_i_pigeon_surjective = n) /\ (((exists ff_h_pigeon_surjective_entry. ff_h_pigeon_surjective_entry + S (fp_value_pigeon_surjective) = S ((S (fp_i_pigeon_surjective)) * c)) /\ exists ff_q_pigeon_surjective_entry. b = ff_q_pigeon_surjective_entry * S ((S (fp_i_pigeon_surjective)) * c) + (fp_value_pigeon_surjective)))))

finite_lt_succ_eq_or_lt · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n
```
le_refl · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= n
```
le_succ · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + a = b) -> exists r. r + a = S b
```
lt_not_le · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + S a = b) -> ~ (exists k. k + b = a)
```

mod_eq_bounded_unique · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b. (exists ha. ha + S a = m) -> (exists hb. hb + S b = m) -> (exists u v. a + m * u = b + m * v) -> a = b

mod_eq_cancel_coprime · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a x y. ~(m = 0) -> (forall d. (exists x. a = d * x) -> (exists y. m = d * y) -> d = 1) -> (exists u v. (a * x) + m * u = (a * y) + m * v) -> exists r s. x + m * r = y + m * s

mod_eq_mul · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b c d. (exists u v. a + m * u = b + m * v) -> (exists r s. c + m * r = d + m * s) -> exists x y. (a * c) + m * x = (b * d) + m * y

mod_eq_refl · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m a. exists u v. a + m * u = a + m * v
```
mod_eq_symm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m a b. (exists u v. a + m * u = b + m * v) -> exists r s. b + m * r = a + m * s
```

mod_eq_trans · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b c. (exists u v. a + m * u = b + m * v) -> (exists r s. b + m * r = c + m * s) -> exists x y. a + m * x = c + m * y

mod_inverse_implies_coprime · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a m z. (exists hmi_left_offset_converse_assumption hmi_right_offset_converse_assumption. a * z + m * hmi_left_offset_converse_assumption = 1 + m * hmi_right_offset_converse_assumption) -> (forall hmi_divisor_converse_result. (exists hmi_left_factor_converse_result. a = hmi_divisor_converse_result * hmi_left_factor_converse_result) -> (exists hmi_right_factor_converse_result. m = hmi_divisor_converse_result * hmi_right_factor_converse_result) -> hmi_divisor_converse_result = 1)

mul_assoc · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m k. (n * m) * k = n * (m * k)
```
mul_comm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m. n * m = m * n
```
mul_one · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n * 1 = n
```
mul_shuffle_four · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b c d. (a * b) * (c * d) = (a * c) * (b * d)
```
one_mul · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. 1 * n = n
```

pow_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a e. exists n. (exists ff_b_x ff_c_x. ((forall ff_i_x_repeat. (exists ff_lt_x_repeat_bound. ff_lt_x_repeat_bound + S ff_i_x_repeat = e) -> (((exists ff_h_x_repeat_decoded. ff_h_x_repeat_decoded + S (a) = S ((S (ff_i_x_repeat)) * ff_c_x)) /\ exists ff_q_x_repeat_decoded. ff_b_x = ff_q_x_repeat_decoded * S ((S (ff_i_x_repeat)) * ff_c_x) + (a)))) /\ (exists ff_u_x_product ff_v_x_product. ((((exists ff_h_x_product_start. ff_h_x_product_start + S (1) = S ((S (0)) * ff_v_x_product)) /\ exists ff_q_x_product_start. ff_u_x_product = ff_q_x_product_start * S ((S (0)) * ff_v_x_product) + (1))) /\ ((((exists ff_h_x_product_terminal. ff_h_x_product_terminal + S (n) = S ((S (e)) * ff_v_x_product)) /\ exists ff_q_x_product_terminal. ff_u_x_product = ff_q_x_product_terminal * S ((S (e)) * ff_v_x_product) + (n))) /\ forall ff_i_x_product. (exists ff_lt_x_product_bound. ff_lt_x_product_bound + S ff_i_x_product = e) -> exists ff_p_x_product ff_r_x_product ff_s_x_product. ((((exists ff_h_x_product_factor. ff_h_x_product_factor + S (ff_p_x_product) = S ((S (ff_i_x_product)) * ff_c_x)) /\ exists ff_q_x_product_factor. ff_b_x = ff_q_x_product_factor * S ((S (ff_i_x_product)) * ff_c_x) + (ff_p_x_product))) /\ ((((exists ff_h_x_product_partial. ff_h_x_product_partial + S (ff_r_x_product) = S ((S (ff_i_x_product)) * ff_v_x_product)) /\ exists ff_q_x_product_partial. ff_u_x_product = ff_q_x_product_partial * S ((S (ff_i_x_product)) * ff_v_x_product) + (ff_r_x_product))) /\ ((((exists ff_h_x_product_successor. ff_h_x_product_successor + S (ff_s_x_product) = S ((S (S ff_i_x_product)) * ff_v_x_product)) /\ exists ff_q_x_product_successor. ff_u_x_product = ff_q_x_product_successor * S ((S (S ff_i_x_product)) * ff_v_x_product) + (ff_s_x_product))) /\ ff_s_x_product = ff_r_x_product * ff_p_x_product))))))))

pow_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a e n m. (exists ff_b_l ff_c_l. ((forall ff_i_l_repeat. (exists ff_lt_l_repeat_bound. ff_lt_l_repeat_bound + S ff_i_l_repeat = e) -> (((exists ff_h_l_repeat_decoded. ff_h_l_repeat_decoded + S (a) = S ((S (ff_i_l_repeat)) * ff_c_l)) /\ exists ff_q_l_repeat_decoded. ff_b_l = ff_q_l_repeat_decoded * S ((S (ff_i_l_repeat)) * ff_c_l) + (a)))) /\ (exists ff_u_l_product ff_v_l_product. ((((exists ff_h_l_product_start. ff_h_l_product_start + S (1) = S ((S (0)) * ff_v_l_product)) /\ exists ff_q_l_product_start. ff_u_l_product = ff_q_l_product_start * S ((S (0)) * ff_v_l_product) + (1))) /\ ((((exists ff_h_l_product_terminal. ff_h_l_product_terminal + S (n) = S ((S (e)) * ff_v_l_product)) /\ exists ff_q_l_product_terminal. ff_u_l_product = ff_q_l_product_terminal * S ((S (e)) * ff_v_l_product) + (n))) /\ forall ff_i_l_product. (exists ff_lt_l_product_bound. ff_lt_l_product_bound + S ff_i_l_product = e) -> exists ff_p_l_product ff_r_l_product ff_s_l_product. ((((exists ff_h_l_product_factor. ff_h_l_product_factor + S (ff_p_l_product) = S ((S (ff_i_l_product)) * ff_c_l)) /\ exists ff_q_l_product_factor. ff_b_l = ff_q_l_product_factor * S ((S (ff_i_l_product)) * ff_c_l) + (ff_p_l_product))) /\ ((((exists ff_h_l_product_partial. ff_h_l_product_partial + S (ff_r_l_product) = S ((S (ff_i_l_product)) * ff_v_l_product)) /\ exists ff_q_l_product_partial. ff_u_l_product = ff_q_l_product_partial * S ((S (ff_i_l_product)) * ff_v_l_product) + (ff_r_l_product))) /\ ((((exists ff_h_l_product_successor. ff_h_l_product_successor + S (ff_s_l_product) = S ((S (S ff_i_l_product)) * ff_v_l_product)) /\ exists ff_q_l_product_successor. ff_u_l_product = ff_q_l_product_successor * S ((S (S ff_i_l_product)) * ff_v_l_product) + (ff_s_l_product))) /\ ff_s_l_product = ff_r_l_product * ff_p_l_product)))))))) -> (exists ff_b_r ff_c_r. ((forall ff_i_r_repeat. (exists ff_lt_r_repeat_bound. ff_lt_r_repeat_bound + S ff_i_r_repeat = e) -> (((exists ff_h_r_repeat_decoded. ff_h_r_repeat_decoded + S (a) = S ((S (ff_i_r_repeat)) * ff_c_r)) /\ exists ff_q_r_repeat_decoded. ff_b_r = ff_q_r_repeat_decoded * S ((S (ff_i_r_repeat)) * ff_c_r) + (a)))) /\ (exists ff_u_r_product ff_v_r_product. ((((exists ff_h_r_product_start. ff_h_r_product_start + S (1) = S ((S (0)) * ff_v_r_product)) /\ exists ff_q_r_product_start. ff_u_r_product = ff_q_r_product_start * S ((S (0)) * ff_v_r_product) + (1))) /\ ((((exists ff_h_r_product_terminal. ff_h_r_product_terminal + S (m) = S ((S (e)) * ff_v_r_product)) /\ exists ff_q_r_product_terminal. ff_u_r_product = ff_q_r_product_terminal * S ((S (e)) * ff_v_r_product) + (m))) /\ forall ff_i_r_product. (exists ff_lt_r_product_bound. ff_lt_r_product_bound + S ff_i_r_product = e) -> exists ff_p_r_product ff_r_r_product ff_s_r_product. ((((exists ff_h_r_product_factor. ff_h_r_product_factor + S (ff_p_r_product) = S ((S (ff_i_r_product)) * ff_c_r)) /\ exists ff_q_r_product_factor. ff_b_r = ff_q_r_product_factor * S ((S (ff_i_r_product)) * ff_c_r) + (ff_p_r_product))) /\ ((((exists ff_h_r_product_partial. ff_h_r_product_partial + S (ff_r_r_product) = S ((S (ff_i_r_product)) * ff_v_r_product)) /\ exists ff_q_r_product_partial. ff_u_r_product = ff_q_r_product_partial * S ((S (ff_i_r_product)) * ff_v_r_product) + (ff_r_r_product))) /\ ((((exists ff_h_r_product_successor. ff_h_r_product_successor + S (ff_s_r_product) = S ((S (S ff_i_r_product)) * ff_v_r_product)) /\ exists ff_q_r_product_successor. ff_u_r_product = ff_q_r_product_successor * S ((S (S ff_i_r_product)) * ff_v_r_product) + (ff_s_r_product))) /\ ff_s_r_product = ff_r_r_product * ff_p_r_product)))))))) -> n = m

pow_successor_pair_mul · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a e se r n. se = S e -> (exists ff_b_pair_predecessor ff_c_pair_predecessor. ((forall ff_i_pair_predecessor_repeat. (exists ff_lt_pair_predecessor_repeat_bound. ff_lt_pair_predecessor_repeat_bound + S ff_i_pair_predecessor_repeat = e) -> (((exists ff_h_pair_predecessor_repeat_decoded. ff_h_pair_predecessor_repeat_decoded + S (a) = S ((S (ff_i_pair_predecessor_repeat)) * ff_c_pair_predecessor)) /\ exists ff_q_pair_predecessor_repeat_decoded. ff_b_pair_predecessor = ff_q_pair_predecessor_repeat_decoded * S ((S (ff_i_pair_predecessor_repeat)) * ff_c_pair_predecessor) + (a)))) /\ (exists ff_u_pair_predecessor_product ff_v_pair_predecessor_product. ((((exists ff_h_pair_predecessor_product_start. ff_h_pair_predecessor_product_start + S (1) = S ((S (0)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_start. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_start * S ((S (0)) * ff_v_pair_predecessor_product) + (1))) /\ ((((exists ff_h_pair_predecessor_product_terminal. ff_h_pair_predecessor_product_terminal + S (r) = S ((S (e)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_terminal. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_terminal * S ((S (e)) * ff_v_pair_predecessor_product) + (r))) /\ forall ff_i_pair_predecessor_product. (exists ff_lt_pair_predecessor_product_bound. ff_lt_pair_predecessor_product_bound + S ff_i_pair_predecessor_product = e) -> exists ff_p_pair_predecessor_product ff_r_pair_predecessor_product ff_s_pair_predecessor_product. ((((exists ff_h_pair_predecessor_product_factor. ff_h_pair_predecessor_product_factor + S (ff_p_pair_predecessor_product) = S ((S (ff_i_pair_predecessor_product)) * ff_c_pair_predecessor)) /\ exists ff_q_pair_predecessor_product_factor. ff_b_pair_predecessor = ff_q_pair_predecessor_product_factor * S ((S (ff_i_pair_predecessor_product)) * ff_c_pair_predecessor) + (ff_p_pair_predecessor_product))) /\ ((((exists ff_h_pair_predecessor_product_partial. ff_h_pair_predecessor_product_partial + S (ff_r_pair_predecessor_product) = S ((S (ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_partial. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_partial * S ((S (ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product) + (ff_r_pair_predecessor_product))) /\ ((((exists ff_h_pair_predecessor_product_successor. ff_h_pair_predecessor_product_successor + S (ff_s_pair_predecessor_product) = S ((S (S ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_successor. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_successor * S ((S (S ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product) + (ff_s_pair_predecessor_product))) /\ ff_s_pair_predecessor_product = ff_r_pair_predecessor_product * ff_p_pair_predecessor_product)))))))) -> (exists ff_b_pair_successor ff_c_pair_successor. ((forall ff_i_pair_successor_repeat. (exists ff_lt_pair_successor_repeat_bound. ff_lt_pair_successor_repeat_bound + S ff_i_pair_successor_repeat = se) -> (((exists ff_h_pair_successor_repeat_decoded. ff_h_pair_successor_repeat_decoded + S (a) = S ((S (ff_i_pair_successor_repeat)) * ff_c_pair_successor)) /\ exists ff_q_pair_successor_repeat_decoded. ff_b_pair_successor = ff_q_pair_successor_repeat_decoded * S ((S (ff_i_pair_successor_repeat)) * ff_c_pair_successor) + (a)))) /\ (exists ff_u_pair_successor_product ff_v_pair_successor_product. ((((exists ff_h_pair_successor_product_start. ff_h_pair_successor_product_start + S (1) = S ((S (0)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_start. ff_u_pair_successor_product = ff_q_pair_successor_product_start * S ((S (0)) * ff_v_pair_successor_product) + (1))) /\ ((((exists ff_h_pair_successor_product_terminal. ff_h_pair_successor_product_terminal + S (n) = S ((S (se)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_terminal. ff_u_pair_successor_product = ff_q_pair_successor_product_terminal * S ((S (se)) * ff_v_pair_successor_product) + (n))) /\ forall ff_i_pair_successor_product. (exists ff_lt_pair_successor_product_bound. ff_lt_pair_successor_product_bound + S ff_i_pair_successor_product = se) -> exists ff_p_pair_successor_product ff_r_pair_successor_product ff_s_pair_successor_product. ((((exists ff_h_pair_successor_product_factor. ff_h_pair_successor_product_factor + S (ff_p_pair_successor_product) = S ((S (ff_i_pair_successor_product)) * ff_c_pair_successor)) /\ exists ff_q_pair_successor_product_factor. ff_b_pair_successor = ff_q_pair_successor_product_factor * S ((S (ff_i_pair_successor_product)) * ff_c_pair_successor) + (ff_p_pair_successor_product))) /\ ((((exists ff_h_pair_successor_product_partial. ff_h_pair_successor_product_partial + S (ff_r_pair_successor_product) = S ((S (ff_i_pair_successor_product)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_partial. ff_u_pair_successor_product = ff_q_pair_successor_product_partial * S ((S (ff_i_pair_successor_product)) * ff_v_pair_successor_product) + (ff_r_pair_successor_product))) /\ ((((exists ff_h_pair_successor_product_successor. ff_h_pair_successor_product_successor + S (ff_s_pair_successor_product) = S ((S (S ff_i_pair_successor_product)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_successor. ff_u_pair_successor_product = ff_q_pair_successor_product_successor * S ((S (S ff_i_pair_successor_product)) * ff_v_pair_successor_product) + (ff_s_pair_successor_product))) /\ ff_s_pair_successor_product = ff_r_pair_successor_product * ff_p_pair_successor_product)))))))) -> n = r * a

pow_zero · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a e n. e = 0 -> (exists ff_b_z ff_c_z. ((forall ff_i_z_repeat. (exists ff_lt_z_repeat_bound. ff_lt_z_repeat_bound + S ff_i_z_repeat = e) -> (((exists ff_h_z_repeat_decoded. ff_h_z_repeat_decoded + S (a) = S ((S (ff_i_z_repeat)) * ff_c_z)) /\ exists ff_q_z_repeat_decoded. ff_b_z = ff_q_z_repeat_decoded * S ((S (ff_i_z_repeat)) * ff_c_z) + (a)))) /\ (exists ff_u_z_product ff_v_z_product. ((((exists ff_h_z_product_start. ff_h_z_product_start + S (1) = S ((S (0)) * ff_v_z_product)) /\ exists ff_q_z_product_start. ff_u_z_product = ff_q_z_product_start * S ((S (0)) * ff_v_z_product) + (1))) /\ ((((exists ff_h_z_product_terminal. ff_h_z_product_terminal + S (n) = S ((S (e)) * ff_v_z_product)) /\ exists ff_q_z_product_terminal. ff_u_z_product = ff_q_z_product_terminal * S ((S (e)) * ff_v_z_product) + (n))) /\ forall ff_i_z_product. (exists ff_lt_z_product_bound. ff_lt_z_product_bound + S ff_i_z_product = e) -> exists ff_p_z_product ff_r_z_product ff_s_z_product. ((((exists ff_h_z_product_factor. ff_h_z_product_factor + S (ff_p_z_product) = S ((S (ff_i_z_product)) * ff_c_z)) /\ exists ff_q_z_product_factor. ff_b_z = ff_q_z_product_factor * S ((S (ff_i_z_product)) * ff_c_z) + (ff_p_z_product))) /\ ((((exists ff_h_z_product_partial. ff_h_z_product_partial + S (ff_r_z_product) = S ((S (ff_i_z_product)) * ff_v_z_product)) /\ exists ff_q_z_product_partial. ff_u_z_product = ff_q_z_product_partial * S ((S (ff_i_z_product)) * ff_v_z_product) + (ff_r_z_product))) /\ ((((exists ff_h_z_product_successor. ff_h_z_product_successor + S (ff_s_z_product) = S ((S (S ff_i_z_product)) * ff_v_z_product)) /\ exists ff_q_z_product_successor. ff_u_z_product = ff_q_z_product_successor * S ((S (S ff_i_z_product)) * ff_v_z_product) + (ff_s_z_product))) /\ ff_s_z_product = ff_r_z_product * ff_p_z_product)))))))) -> n = 1

remainder_decomposition_to_mod_eq · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m b q x. b = q * m + x -> exists u v. b + m * u = x + m * v
```

totient_coprime_cancel_unit_factor · checked inherited prerequisite

Exact statement in the checked dependency cone

forall p n a. (forall eut_divisor_cancel_unit. (exists eut_left_cancel_unit. (p) = eut_divisor_cancel_unit * eut_left_cancel_unit) -> (exists eut_right_cancel_unit. (n) = eut_divisor_cancel_unit * eut_right_cancel_unit) -> eut_divisor_cancel_unit = 1) -> ((((forall eut_divisor_cancel_predicate_left. (exists eut_left_cancel_predicate_left. (p*a) = eut_divisor_cancel_predicate_left * eut_left_cancel_predicate_left) -> (exists eut_right_cancel_predicate_left. (n) = eut_divisor_cancel_predicate_left * eut_right_cancel_predicate_left) -> eut_divisor_cancel_predicate_left = 1) -> (forall eut_divisor_cancel_predicate_right. (exists eut_left_cancel_predicate_right. (a) = eut_divisor_cancel_predicate_right * eut_left_cancel_predicate_right) -> (exists eut_right_cancel_predicate_right. (n) = eut_divisor_cancel_predicate_right * eut_right_cancel_predicate_right) -> eut_divisor_cancel_predicate_right = 1)) /\ ((forall eut_divisor_cancel_predicate_right. (exists eut_left_cancel_predicate_right. (a) = eut_divisor_cancel_predicate_right * eut_left_cancel_predicate_right) -> (exists eut_right_cancel_predicate_right. (n) = eut_divisor_cancel_predicate_right * eut_right_cancel_predicate_right) -> eut_divisor_cancel_predicate_right = 1) -> (forall eut_divisor_cancel_predicate_left. (exists eut_left_cancel_predicate_left. (p*a) = eut_divisor_cancel_predicate_left * eut_left_cancel_predicate_left) -> (exists eut_right_cancel_predicate_left. (n) = eut_divisor_cancel_predicate_left * eut_right_cancel_predicate_left) -> eut_divisor_cancel_predicate_left = 1))))

totient_coprime_decidable · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a n. (forall eut_divisor_dec_yes. (exists eut_left_dec_yes. (a) = eut_divisor_dec_yes * eut_left_dec_yes) -> (exists eut_right_dec_yes. (n) = eut_divisor_dec_yes * eut_right_dec_yes) -> eut_divisor_dec_yes = 1) \/ ~(forall eut_divisor_dec_no. (exists eut_left_dec_no. (a) = eut_divisor_dec_no * eut_left_dec_no) -> (exists eut_right_dec_no. (n) = eut_divisor_dec_no * eut_right_dec_no) -> eut_divisor_dec_no = 1)

totient_coprime_periodic · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n k a. (((forall eut_divisor_periodic_left. (exists eut_left_periodic_left. (n*k+a) = eut_divisor_periodic_left * eut_left_periodic_left) -> (exists eut_right_periodic_left. (n) = eut_divisor_periodic_left * eut_right_periodic_left) -> eut_divisor_periodic_left = 1) -> (forall eut_divisor_periodic_right. (exists eut_left_periodic_right. (a) = eut_divisor_periodic_right * eut_left_periodic_right) -> (exists eut_right_periodic_right. (n) = eut_divisor_periodic_right * eut_right_periodic_right) -> eut_divisor_periodic_right = 1)) /\ ((forall eut_divisor_periodic_right. (exists eut_left_periodic_right. (a) = eut_divisor_periodic_right * eut_left_periodic_right) -> (exists eut_right_periodic_right. (n) = eut_divisor_periodic_right * eut_right_periodic_right) -> eut_divisor_periodic_right = 1) -> (forall eut_divisor_periodic_left. (exists eut_left_periodic_left. (n*k+a) = eut_divisor_periodic_left * eut_left_periodic_left) -> (exists eut_right_periodic_left. (n) = eut_divisor_periodic_left * eut_right_periodic_left) -> eut_divisor_periodic_left = 1)))

totient_unit_count_succ_decompose · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n l t. (exists eut_code_succ_count eut_scale_succ_count. (forall eut_index_succ_count_mask. (exists eut_gap_succ_count_mask_bound. eut_gap_succ_count_mask_bound + S (eut_index_succ_count_mask) = (S l)) -> exists eut_bit_succ_count_mask. (((exists fs_h_eut_succ_count_mask_entry. fs_h_eut_succ_count_mask_entry + S (eut_bit_succ_count_mask) = S ((S (eut_index_succ_count_mask)) * eut_scale_succ_count)) /\ exists fs_q_eut_succ_count_mask_entry. eut_code_succ_count = fs_q_eut_succ_count_mask_entry * S ((S (eut_index_succ_count_mask)) * eut_scale_succ_count) + (eut_bit_succ_count_mask))) /\ ((((forall eut_divisor_succ_count_mask_choice_coprime. (exists eut_left_succ_count_mask_choice_coprime. (eut_index_succ_count_mask) = eut_divisor_succ_count_mask_choice_coprime * eut_left_succ_count_mask_choice_coprime) -> (exists eut_right_succ_count_mask_choice_coprime. (n) = eut_divisor_succ_count_mask_choice_coprime * eut_right_succ_count_mask_choice_coprime) -> eut_divisor_succ_count_mask_choice_coprime = 1) /\ (eut_bit_succ_count_mask) = 1) \/ (~(forall eut_divisor_succ_count_mask_choice_coprime. (exists eut_left_succ_count_mask_choice_coprime. (eut_index_succ_count_mask) = eut_divisor_succ_count_mask_choice_coprime * eut_left_succ_count_mask_choice_coprime) -> (exists eut_right_succ_count_mask_choice_coprime. (n) = eut_divisor_succ_count_mask_choice_coprime * eut_right_succ_count_mask_choice_coprime) -> eut_divisor_succ_count_mask_choice_coprime = 1) /\ (eut_bit_succ_count_mask) = 0)))) /\ (exists fs_u_eut_succ_count_sum fs_v_eut_succ_count_sum. ((((exists fs_h_eut_succ_count_sum_body_start. fs_h_eut_succ_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_succ_count_sum)) /\ exists fs_q_eut_succ_count_sum_body_start. fs_u_eut_succ_count_sum = fs_q_eut_succ_count_sum_body_start * S ((S (0)) * fs_v_eut_succ_count_sum) + (0))) /\ ((((exists fs_h_eut_succ_count_sum_body_terminal. fs_h_eut_succ_count_sum_body_terminal + S (t) = S ((S (S l)) * fs_v_eut_succ_count_sum)) /\ exists fs_q_eut_succ_count_sum_body_terminal. fs_u_eut_succ_count_sum = fs_q_eut_succ_count_sum_body_terminal * S ((S (S l)) * fs_v_eut_succ_count_sum) + (t))) /\ forall fs_i_eut_succ_count_sum_body_steps. (exists fs_lt_eut_succ_count_sum_body_steps_bound. fs_lt_eut_succ_count_sum_body_steps_bound + S fs_i_eut_succ_count_sum_body_steps = S l) -> exists fs_a_eut_succ_count_sum_body_steps fs_r_eut_succ_count_sum_body_steps fs_s_eut_succ_count_sum_body_steps. ((((exists fs_h_eut_succ_count_sum_body_steps_summand. fs_h_eut_succ_count_sum_body_steps_summand + S (fs_a_eut_succ_count_sum_body_steps) = S ((S (fs_i_eut_succ_count_sum_body_steps)) * eut_scale_succ_count)) /\ exists fs_q_eut_succ_count_sum_body_steps_summand. eut_code_succ_count = fs_q_eut_succ_count_sum_body_steps_summand * S ((S (fs_i_eut_succ_count_sum_body_steps)) * eut_scale_succ_count) + (fs_a_eut_succ_count_sum_body_steps))) /\ ((((exists fs_h_eut_succ_count_sum_body_steps_partial. fs_h_eut_succ_count_sum_body_steps_partial + S (fs_r_eut_succ_count_sum_body_steps) = S ((S (fs_i_eut_succ_count_sum_body_steps)) * fs_v_eut_succ_count_sum)) /\ exists fs_q_eut_succ_count_sum_body_steps_partial. fs_u_eut_succ_count_sum = fs_q_eut_succ_count_sum_body_steps_partial * S ((S (fs_i_eut_succ_count_sum_body_steps)) * fs_v_eut_succ_count_sum) + (fs_r_eut_succ_count_sum_body_steps))) /\ ((((exists fs_h_eut_succ_count_sum_body_steps_successor. fs_h_eut_succ_count_sum_body_steps_successor + S (fs_s_eut_succ_count_sum_body_steps) = S ((S (S fs_i_eut_succ_count_sum_body_steps)) * fs_v_eut_succ_count_sum)) /\ exists fs_q_eut_succ_count_sum_body_steps_successor. fs_u_eut_succ_count_sum = fs_q_eut_succ_count_sum_body_steps_successor * S ((S (S fs_i_eut_succ_count_sum_body_steps)) * fs_v_eut_succ_count_sum) + (fs_s_eut_succ_count_sum_body_steps))) /\ fs_s_eut_succ_count_sum_body_steps = fs_r_eut_succ_count_sum_body_steps + fs_a_eut_succ_count_sum_body_steps))))))) -> exists r e. (exists eut_code_succ_previous eut_scale_succ_previous. (forall eut_index_succ_previous_mask. (exists eut_gap_succ_previous_mask_bound. eut_gap_succ_previous_mask_bound + S (eut_index_succ_previous_mask) = (l)) -> exists eut_bit_succ_previous_mask. (((exists fs_h_eut_succ_previous_mask_entry. fs_h_eut_succ_previous_mask_entry + S (eut_bit_succ_previous_mask) = S ((S (eut_index_succ_previous_mask)) * eut_scale_succ_previous)) /\ exists fs_q_eut_succ_previous_mask_entry. eut_code_succ_previous = fs_q_eut_succ_previous_mask_entry * S ((S (eut_index_succ_previous_mask)) * eut_scale_succ_previous) + (eut_bit_succ_previous_mask))) /\ ((((forall eut_divisor_succ_previous_mask_choice_coprime. (exists eut_left_succ_previous_mask_choice_coprime. (eut_index_succ_previous_mask) = eut_divisor_succ_previous_mask_choice_coprime * eut_left_succ_previous_mask_choice_coprime) -> (exists eut_right_succ_previous_mask_choice_coprime. (n) = eut_divisor_succ_previous_mask_choice_coprime * eut_right_succ_previous_mask_choice_coprime) -> eut_divisor_succ_previous_mask_choice_coprime = 1) /\ (eut_bit_succ_previous_mask) = 1) \/ (~(forall eut_divisor_succ_previous_mask_choice_coprime. (exists eut_left_succ_previous_mask_choice_coprime. (eut_index_succ_previous_mask) = eut_divisor_succ_previous_mask_choice_coprime * eut_left_succ_previous_mask_choice_coprime) -> (exists eut_right_succ_previous_mask_choice_coprime. (n) = eut_divisor_succ_previous_mask_choice_coprime * eut_right_succ_previous_mask_choice_coprime) -> eut_divisor_succ_previous_mask_choice_coprime = 1) /\ (eut_bit_succ_previous_mask) = 0)))) /\ (exists fs_u_eut_succ_previous_sum fs_v_eut_succ_previous_sum. ((((exists fs_h_eut_succ_previous_sum_body_start. fs_h_eut_succ_previous_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_succ_previous_sum)) /\ exists fs_q_eut_succ_previous_sum_body_start. fs_u_eut_succ_previous_sum = fs_q_eut_succ_previous_sum_body_start * S ((S (0)) * fs_v_eut_succ_previous_sum) + (0))) /\ ((((exists fs_h_eut_succ_previous_sum_body_terminal. fs_h_eut_succ_previous_sum_body_terminal + S (r) = S ((S (l)) * fs_v_eut_succ_previous_sum)) /\ exists fs_q_eut_succ_previous_sum_body_terminal. fs_u_eut_succ_previous_sum = fs_q_eut_succ_previous_sum_body_terminal * S ((S (l)) * fs_v_eut_succ_previous_sum) + (r))) /\ forall fs_i_eut_succ_previous_sum_body_steps. (exists fs_lt_eut_succ_previous_sum_body_steps_bound. fs_lt_eut_succ_previous_sum_body_steps_bound + S fs_i_eut_succ_previous_sum_body_steps = l) -> exists fs_a_eut_succ_previous_sum_body_steps fs_r_eut_succ_previous_sum_body_steps fs_s_eut_succ_previous_sum_body_steps. ((((exists fs_h_eut_succ_previous_sum_body_steps_summand. fs_h_eut_succ_previous_sum_body_steps_summand + S (fs_a_eut_succ_previous_sum_body_steps) = S ((S (fs_i_eut_succ_previous_sum_body_steps)) * eut_scale_succ_previous)) /\ exists fs_q_eut_succ_previous_sum_body_steps_summand. eut_code_succ_previous = fs_q_eut_succ_previous_sum_body_steps_summand * S ((S (fs_i_eut_succ_previous_sum_body_steps)) * eut_scale_succ_previous) + (fs_a_eut_succ_previous_sum_body_steps))) /\ ((((exists fs_h_eut_succ_previous_sum_body_steps_partial. fs_h_eut_succ_previous_sum_body_steps_partial + S (fs_r_eut_succ_previous_sum_body_steps) = S ((S (fs_i_eut_succ_previous_sum_body_steps)) * fs_v_eut_succ_previous_sum)) /\ exists fs_q_eut_succ_previous_sum_body_steps_partial. fs_u_eut_succ_previous_sum = fs_q_eut_succ_previous_sum_body_steps_partial * S ((S (fs_i_eut_succ_previous_sum_body_steps)) * fs_v_eut_succ_previous_sum) + (fs_r_eut_succ_previous_sum_body_steps))) /\ ((((exists fs_h_eut_succ_previous_sum_body_steps_successor. fs_h_eut_succ_previous_sum_body_steps_successor + S (fs_s_eut_succ_previous_sum_body_steps) = S ((S (S fs_i_eut_succ_previous_sum_body_steps)) * fs_v_eut_succ_previous_sum)) /\ exists fs_q_eut_succ_previous_sum_body_steps_successor. fs_u_eut_succ_previous_sum = fs_q_eut_succ_previous_sum_body_steps_successor * S ((S (S fs_i_eut_succ_previous_sum_body_steps)) * fs_v_eut_succ_previous_sum) + (fs_s_eut_succ_previous_sum_body_steps))) /\ fs_s_eut_succ_previous_sum_body_steps = fs_r_eut_succ_previous_sum_body_steps + fs_a_eut_succ_previous_sum_body_steps))))))) /\ (((((forall eut_divisor_succ_choice_coprime. (exists eut_left_succ_choice_coprime. (l) = eut_divisor_succ_choice_coprime * eut_left_succ_choice_coprime) -> (exists eut_right_succ_choice_coprime. (n) = eut_divisor_succ_choice_coprime * eut_right_succ_choice_coprime) -> eut_divisor_succ_choice_coprime = 1) /\ (e) = 1) \/ (~(forall eut_divisor_succ_choice_coprime. (exists eut_left_succ_choice_coprime. (l) = eut_divisor_succ_choice_coprime * eut_left_succ_choice_coprime) -> (exists eut_right_succ_choice_coprime. (n) = eut_divisor_succ_choice_coprime * eut_right_succ_choice_coprime) -> eut_divisor_succ_choice_coprime = 1) /\ (e) = 0))) /\ t=r+e)

totient_unit_count_zero_length · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n t. (exists eut_code_empty_count eut_scale_empty_count. (forall eut_index_empty_count_mask. (exists eut_gap_empty_count_mask_bound. eut_gap_empty_count_mask_bound + S (eut_index_empty_count_mask) = (0)) -> exists eut_bit_empty_count_mask. (((exists fs_h_eut_empty_count_mask_entry. fs_h_eut_empty_count_mask_entry + S (eut_bit_empty_count_mask) = S ((S (eut_index_empty_count_mask)) * eut_scale_empty_count)) /\ exists fs_q_eut_empty_count_mask_entry. eut_code_empty_count = fs_q_eut_empty_count_mask_entry * S ((S (eut_index_empty_count_mask)) * eut_scale_empty_count) + (eut_bit_empty_count_mask))) /\ ((((forall eut_divisor_empty_count_mask_choice_coprime. (exists eut_left_empty_count_mask_choice_coprime. (eut_index_empty_count_mask) = eut_divisor_empty_count_mask_choice_coprime * eut_left_empty_count_mask_choice_coprime) -> (exists eut_right_empty_count_mask_choice_coprime. (n) = eut_divisor_empty_count_mask_choice_coprime * eut_right_empty_count_mask_choice_coprime) -> eut_divisor_empty_count_mask_choice_coprime = 1) /\ (eut_bit_empty_count_mask) = 1) \/ (~(forall eut_divisor_empty_count_mask_choice_coprime. (exists eut_left_empty_count_mask_choice_coprime. (eut_index_empty_count_mask) = eut_divisor_empty_count_mask_choice_coprime * eut_left_empty_count_mask_choice_coprime) -> (exists eut_right_empty_count_mask_choice_coprime. (n) = eut_divisor_empty_count_mask_choice_coprime * eut_right_empty_count_mask_choice_coprime) -> eut_divisor_empty_count_mask_choice_coprime = 1) /\ (eut_bit_empty_count_mask) = 0)))) /\ (exists fs_u_eut_empty_count_sum fs_v_eut_empty_count_sum. ((((exists fs_h_eut_empty_count_sum_body_start. fs_h_eut_empty_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_empty_count_sum)) /\ exists fs_q_eut_empty_count_sum_body_start. fs_u_eut_empty_count_sum = fs_q_eut_empty_count_sum_body_start * S ((S (0)) * fs_v_eut_empty_count_sum) + (0))) /\ ((((exists fs_h_eut_empty_count_sum_body_terminal. fs_h_eut_empty_count_sum_body_terminal + S (t) = S ((S (0)) * fs_v_eut_empty_count_sum)) /\ exists fs_q_eut_empty_count_sum_body_terminal. fs_u_eut_empty_count_sum = fs_q_eut_empty_count_sum_body_terminal * S ((S (0)) * fs_v_eut_empty_count_sum) + (t))) /\ forall fs_i_eut_empty_count_sum_body_steps. (exists fs_lt_eut_empty_count_sum_body_steps_bound. fs_lt_eut_empty_count_sum_body_steps_bound + S fs_i_eut_empty_count_sum_body_steps = 0) -> exists fs_a_eut_empty_count_sum_body_steps fs_r_eut_empty_count_sum_body_steps fs_s_eut_empty_count_sum_body_steps. ((((exists fs_h_eut_empty_count_sum_body_steps_summand. fs_h_eut_empty_count_sum_body_steps_summand + S (fs_a_eut_empty_count_sum_body_steps) = S ((S (fs_i_eut_empty_count_sum_body_steps)) * eut_scale_empty_count)) /\ exists fs_q_eut_empty_count_sum_body_steps_summand. eut_code_empty_count = fs_q_eut_empty_count_sum_body_steps_summand * S ((S (fs_i_eut_empty_count_sum_body_steps)) * eut_scale_empty_count) + (fs_a_eut_empty_count_sum_body_steps))) /\ ((((exists fs_h_eut_empty_count_sum_body_steps_partial. fs_h_eut_empty_count_sum_body_steps_partial + S (fs_r_eut_empty_count_sum_body_steps) = S ((S (fs_i_eut_empty_count_sum_body_steps)) * fs_v_eut_empty_count_sum)) /\ exists fs_q_eut_empty_count_sum_body_steps_partial. fs_u_eut_empty_count_sum = fs_q_eut_empty_count_sum_body_steps_partial * S ((S (fs_i_eut_empty_count_sum_body_steps)) * fs_v_eut_empty_count_sum) + (fs_r_eut_empty_count_sum_body_steps))) /\ ((((exists fs_h_eut_empty_count_sum_body_steps_successor. fs_h_eut_empty_count_sum_body_steps_successor + S (fs_s_eut_empty_count_sum_body_steps) = S ((S (S fs_i_eut_empty_count_sum_body_steps)) * fs_v_eut_empty_count_sum)) /\ exists fs_q_eut_empty_count_sum_body_steps_successor. fs_u_eut_empty_count_sum = fs_q_eut_empty_count_sum_body_steps_successor * S ((S (S fs_i_eut_empty_count_sum_body_steps)) * fs_v_eut_empty_count_sum) + (fs_s_eut_empty_count_sum_body_steps))) /\ fs_s_eut_empty_count_sum_body_steps = fs_r_eut_empty_count_sum_body_steps + fs_a_eut_empty_count_sum_body_steps))))))) -> t=0

zero_le · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. 0 <= n
```