Original: If f is the Gödel mapping and if formula C can be derived from formulas A and B through an inference rule r ; i.e.
Simplified: g_r ( f ( A ) , h ( B ) ) = f ( C ) .