BinaryModularExecution(d,s,a,m,n,r)

Hygienic expanded first-order definition

exists ff_trace_code_be_transport ff_trace_scale_be_transport. ((((((exists ff_h_be_transport_trace_start. ff_h_be_transport_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_transport)) /\ exists ff_q_be_transport_trace_start. ff_trace_code_be_transport = ff_q_be_transport_trace_start * S ((S (0)) * ff_trace_scale_be_transport) + (1))) /\ forall ff_index_be_transport_trace. (exists ff_lt_be_transport_trace_bound. ff_lt_be_transport_trace_bound + S ff_index_be_transport_trace = n) -> exists ff_digit_be_transport_trace ff_previous_be_transport_trace ff_current_be_transport_trace. ((((exists ff_h_be_transport_trace_source. ff_h_be_transport_trace_source + S (ff_digit_be_transport_trace) = S ((S (ff_index_be_transport_trace)) * s)) /\ exists ff_q_be_transport_trace_source. d = ff_q_be_transport_trace_source * S ((S (ff_index_be_transport_trace)) * s) + (ff_digit_be_transport_trace))) /\ ((((exists ff_h_be_transport_trace_before. ff_h_be_transport_trace_before + S (ff_previous_be_transport_trace) = S ((S (ff_index_be_transport_trace)) * ff_trace_scale_be_transport)) /\ exists ff_q_be_transport_trace_before. ff_trace_code_be_transport = ff_q_be_transport_trace_before * S ((S (ff_index_be_transport_trace)) * ff_trace_scale_be_transport) + (ff_previous_be_transport_trace))) /\ ((((exists ff_h_be_transport_trace_after. ff_h_be_transport_trace_after + S (ff_current_be_transport_trace) = S ((S (S ff_index_be_transport_trace)) * ff_trace_scale_be_transport)) /\ exists ff_q_be_transport_trace_after. ff_trace_code_be_transport = ff_q_be_transport_trace_after * S ((S (S ff_index_be_transport_trace)) * ff_trace_scale_be_transport) + (ff_current_be_transport_trace))) /\ ((((ff_digit_be_transport_trace = 0) /\ (((exists ff_gap_binary_be_transport_trace_transition_square. ff_gap_binary_be_transport_trace_transition_square + S (ff_current_be_transport_trace) = m) /\ (exists ff_left_binary_be_transport_trace_transition_square_congruence ff_right_binary_be_transport_trace_transition_square_congruence. (ff_previous_be_transport_trace * ff_previous_be_transport_trace) + m * ff_left_binary_be_transport_trace_transition_square_congruence = (ff_current_be_transport_trace) + m * ff_right_binary_be_transport_trace_transition_square_congruence)))) \/ ((ff_digit_be_transport_trace = 1) /\ (((exists ff_gap_binary_be_transport_trace_transition_multiply. ff_gap_binary_be_transport_trace_transition_multiply + S (ff_current_be_transport_trace) = m) /\ (exists ff_left_binary_be_transport_trace_transition_multiply_congruence ff_right_binary_be_transport_trace_transition_multiply_congruence. ((ff_previous_be_transport_trace * ff_previous_be_transport_trace) * a) + m * ff_left_binary_be_transport_trace_transition_multiply_congruence = (ff_current_be_transport_trace) + m * ff_right_binary_be_transport_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_transport_terminal. ff_h_be_transport_terminal + S (r) = S ((S (n)) * ff_trace_scale_be_transport)) /\ exists ff_q_be_transport_terminal. ff_trace_code_be_transport = ff_q_be_transport_terminal * S ((S (n)) * ff_trace_scale_be_transport) + (r))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Definitions depending on this notation

Checked theorems using this definition