formula
rank
Sections
ClassicalProps(jlc)
Doc
Def
= b == b
is mentioned by
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); )
[formula_rank]
In prior sections:
list
3
jlc
Try larger context:
ClassicalProps(jlc)
formula
rank
Sections
ClassicalProps(jlc)
Doc