ALS (All-Substitution) limits formulas that are quantitized with all symbols by certain special names.
Example 1 a1 : (All x)(f(x)) by ....;
Example 2 a1 : (All x)(All y)(f(x,y) and y(a))
In example 2, variable y is also a function name (accordingly, such function form as y(a) appears). Therefore, this is the so called second level predicate logic, but in THEAX, level is not too much of a problem. Also, y is replaced by B(k). B is a functional.
Example 3 a1 : (All x)(All y)(u (x,y)) by ..;
Example 4 a1 : (All x)(f(x) imp g(x)) by ..;
Such as this, when ALS's arguments are 2, computers automatically connect formulas a2 and a3 with imp and inspect if that formula is derived from a1. Instead of a3 above, writing over 2 lines like the following will have the same effect.
Furthermore, when the meaning of formulas differ due to, for example, change of operating order for limiting variables of all symbols, one needs to be careful because the replacement of variables will not be possible.
Example 5 (Abominable) a1 : (All x)(x and b) by ....;
Example 6 (Abominable) a1 : (All f)(f(s) imp g) by ....;
Concerning quantitization blocks, sometimes, ALS or later explained FLW are used in the line following the beginning of a quantitization block. In many cases, using either one is acceptable. Therefore, in following formulas,
we let a1 stay the same and make a2 and a3 like below.
The former means to limit to special x as variables, and the latter means when connecting the beginning of a2 with the formula a3 and parenthesize it, it becomes formula a1.