BinaryExecutionTrace(d,s,a,m,n,h,t)

Hygienic expanded first-order definition

((((exists ff_h_be_transport_start. ff_h_be_transport_start + S (1) = S ((S (0)) * t)) /\ exists ff_q_be_transport_start. h = ff_q_be_transport_start * S ((S (0)) * t) + (1))) /\ forall ff_index_be_transport. (exists ff_lt_be_transport_bound. ff_lt_be_transport_bound + S ff_index_be_transport = n) -> exists ff_digit_be_transport ff_previous_be_transport ff_current_be_transport. ((((exists ff_h_be_transport_source. ff_h_be_transport_source + S (ff_digit_be_transport) = S ((S (ff_index_be_transport)) * s)) /\ exists ff_q_be_transport_source. d = ff_q_be_transport_source * S ((S (ff_index_be_transport)) * s) + (ff_digit_be_transport))) /\ ((((exists ff_h_be_transport_before. ff_h_be_transport_before + S (ff_previous_be_transport) = S ((S (ff_index_be_transport)) * t)) /\ exists ff_q_be_transport_before. h = ff_q_be_transport_before * S ((S (ff_index_be_transport)) * t) + (ff_previous_be_transport))) /\ ((((exists ff_h_be_transport_after. ff_h_be_transport_after + S (ff_current_be_transport) = S ((S (S ff_index_be_transport)) * t)) /\ exists ff_q_be_transport_after. h = ff_q_be_transport_after * S ((S (S ff_index_be_transport)) * t) + (ff_current_be_transport))) /\ ((((ff_digit_be_transport = 0) /\ (((exists ff_gap_binary_be_transport_transition_square. ff_gap_binary_be_transport_transition_square + S (ff_current_be_transport) = m) /\ (exists ff_left_binary_be_transport_transition_square_congruence ff_right_binary_be_transport_transition_square_congruence. (ff_previous_be_transport * ff_previous_be_transport) + m * ff_left_binary_be_transport_transition_square_congruence = (ff_current_be_transport) + m * ff_right_binary_be_transport_transition_square_congruence)))) \/ ((ff_digit_be_transport = 1) /\ (((exists ff_gap_binary_be_transport_transition_multiply. ff_gap_binary_be_transport_transition_multiply + S (ff_current_be_transport) = m) /\ (exists ff_left_binary_be_transport_transition_multiply_congruence ff_right_binary_be_transport_transition_multiply_congruence. ((ff_previous_be_transport * ff_previous_be_transport) * a) + m * ff_left_binary_be_transport_transition_multiply_congruence = (ff_current_be_transport) + m * ff_right_binary_be_transport_transition_multiply_congruence))))))))))

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