Def  i=j == if i=j true ; false fi

is mentioned by

Def  split_factor1(g; x)(u) Def  == if u=x g(x)+g(xx)+g(xx) ; u=xx 0 else g(u) fi	[split_factor1]
Def  split_factor2(g; x; y)(u) Def  == if u=x g(x)+g(xy) ; u=y g(y)+g(xy) ; u=xy 0 else g(u) fi	[split_factor2]
Def  reduce_factorization(f; j)(i) == if i=j f(i)-1 else f(i) fi	[reduce_factorization]
Def  trivial_factorization(z)(i) == if i=z 1 else 0 fi	[trivial_factorization]

In prior sections: bool 1 LogicSupplement int 2 num thy 1

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html