normalization
Sections
ClassicalProps(jlc)
Doc
Def
== (letrec formula_rank f = case f:
x
0;
p
(formula_rank(p)+1); p
q
(formula_rank(p)+formula_rank(q)+1); p
q
(formula_rank(p)+formula_rank(q)+1); p
q
(formula_rank(p)+formula_rank(q)+1); )
In prior sections:
sequent
rank
== (letrec formula_rank f = case f:
x
0;
