MatrixAffineSlice(b,c,s,d,u,v,l)

Hygienic expanded first-order definition

forall ff_index_mcp_advanced ff_source_mcp_advanced ff_target_mcp_advanced. (exists mcp_gap_advanced_bound. mcp_gap_advanced_bound + S (ff_index_mcp_advanced) = (l)) -> (((exists fs_h_mcp_advanced_source. fs_h_mcp_advanced_source + S (ff_source_mcp_advanced) = S ((S ((s) + (d) * ff_index_mcp_advanced)) * c)) /\ exists fs_q_mcp_advanced_source. b = fs_q_mcp_advanced_source * S ((S ((s) + (d) * ff_index_mcp_advanced)) * c) + (ff_source_mcp_advanced))) -> (((exists fs_h_mcp_advanced_target. fs_h_mcp_advanced_target + S (ff_target_mcp_advanced) = S ((S (ff_index_mcp_advanced)) * v)) /\ exists fs_q_mcp_advanced_target. u = fs_q_mcp_advanced_target * S ((S (ff_index_mcp_advanced)) * v) + (ff_target_mcp_advanced))) -> ff_target_mcp_advanced = ff_source_mcp_advanced

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