== (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); ) x varC(x);p1 notC(p1);p2p3 andC(p2;p3);p4p5 orC(p4;p5);p6p7 impC(p6;p7); == InjCase(F; x. varC(x); F. InjCase(F; p1. notC(p1); F. InjCase(F; x. x/p2,p3. andC(p2;p3); F. InjCase(F; x. x/p4,p5. orC(p4;p5), x/p6,p7. impC(p6;p7)))))
is mentioned by
| Def == (letrec formula_rank f = case f:x 0;p (formula_rank(p)+1);pq (formula_rank(p)+formula_rank(q)+1);pq (formula_rank(p)+formula_rank(q)+1);pq (formula_rank(p)+formula_rank(q)+1); ) | [formula_rank] |
In prior sections: formula
Try larger context:
ClassicalProps(jlc)