equal: (3)

ONCE_DEPTH_CONV c applies c
to only the first suitable subterm(s)
found in a top-down search,
i.e. the outermost subterm(s).

# ONCE_DEPTH_CONV BETA_CONV `(\x. x+1) ((\y. y+2) 3)`;;
val it : thm = |- (\x. x + 1) ((\y. y + 2) 3) = (\y. y + 2) 3 + 1
# ONCE_DEPTH_CONV num_CONV `(\x y. x+y) 1 a`;;
val it : thm = |- (\x y. x + y) 1 a = (\x y. x + y) (SUC 0) a

以下の`(\y x. 1 + y x) (\z. z) 2`は，２つの引数(\z. z) 2に対する関数値であることに注意します．

ONCE_DEPTH_CONVでは一番外の\yのみが書き換えられます．

# ONCE_DEPTH_CONV BETA_CONV `(\y x. 1 + y x) (\z. z) 2`;;
val it : thm = |- (\y x. 1 + y x) (\z. z) 2 = (\x. 1 + (\z. z) x) 2

DEPTH_CONV c repeatedly rewrites with c
(in a single bottom-up sweep).
それに対してDEPTH_CONV BETA_CONVでは，内側から\x \yの順に書き換えられますが，1 + (\z. z) 2はBETA_CONVできないのでそこまでとなります．

# DEPTH_CONV BETA_CONV `(\y x. 1 + y x) (\z. z) 2`;;
val it : thm = |- (\y x. 1 + y x) (\z. z) 2 = 1 + (\z. z) 2

REDEPTH_CONV c rewrites with c
(in a bottom-up sweep); after any successful rewrite,
it starts over again at the leaves of the new term.
一方，REDEPTH_CONVでは，1 + (\z. z) 2をもう一度内側からsweepして書き換えるので，(\z. z) 2が2に書き換えれます．

# REDEPTH_CONV BETA_CONV `(\y x. 1 + y x) (\z. z) 2`;;
val it : thm = |- (\y x. 1 + y x) (\z. z) 2 = 1 + 2

TOP_DEPTH_CONV and REDEPTH_CONV repeatedly apply a conversion until no more applications are possible anywhere in the term. The main difference is that TOP_DEPTH_CONV proceeds top-down, whereas
REDEPTH_CONV proceeds bottom-up.

TOP_SWEEP_CONV c rewrite with c top-to-bottom; something like:(rewrite current until no change) then rewrite children with TOP_SWEEP_CONV.
Once the subterms are dealt with, it does not, unlike
TOP_DEPTH_CONV conv, return to re-examine them.
以下の例では，一番外の\yに従う(\z. (\w. w) z) xのみが書き換えられています．

# TOP_SWEEP_CONV BETA_CONV `(\y x. 1 + y x) (\z. (\w. w)z ) 2`;;
val it : thm = |- (\y x. 1 + y x) (\z. (\w. w) z) 2 = (\x. 1 + x) 2

以上まとめると
top->bottom
ONCE_DEPTH_CONV(1st one only),
TOP_SWEEP_CONV(1st system only),
TOP_DEPTH_CONV(all)
bottom->top
DEPTH_CONV(1st system only),
REDEPTH_CONV(all)
となります．

DEPTH_BINOP_CONV op c
For example, DEPTH_BINOP_CONV `+` c rewrites
x,y,z,w in `(x + ( (y + z) + w) )`
(fails if any of these rewrites fail)

# DEPTH_BINOP_CONV `(+):num->num->num` NUM_REDUCE_CONV `(1+2*3+4)+(1+(2-3)*4)+(FACT 10)`;;
val it : thm =
|- (1 + 2 * 3 + 4) + (1 + (2 - 3) * 4) + FACT 10 =
(1 + 6 + 4) + (1 + 0) + 3628800

PATH_CONV path c
For example, PATH_CONV ["b";"l";"r";"r"] (or "blrr") c rewrites the operand of the operand of the operator of the abstraction body with c.

# rator `(1+2)+(3+4)+(5+6)`;;
val it : term = `(+) (1 + 2)`
# rator it;;
val it : term = `(+)`

なので

# PATH_CONV "ll" NUM_REDUCE_CONV `(1+2)+(3+4)+(5+6)`;;
val it : thm = |- (1 + 2) + (3 + 4) + 5 + 6 = (1 + 2) + (3 + 4) + 5 + 6
# PATH_CONV "lr" NUM_REDUCE_CONV `(1+2)+(3+4)+(5+6)`;;
val it : thm = |- (1 + 2) + (3 + 4) + 5 + 6 = 3 + (3 + 4) + 5 + 6
# PATH_CONV "rl" NUM_REDUCE_CONV `(1+2)+(3+4)+(5+6)`;;
val it : thm = |- (1 + 2) + (3 + 4) + 5 + 6 = (1 + 2) + 7 + 5 + 6
# PATH_CONV "rr" NUM_REDUCE_CONV `(1+2)+(3+4)+(5+6)`;;
val it : thm = |- (1 + 2) + (3 + 4) + 5 + 6 = (1 + 2) + (3 + 4) + 11