:: deftheorem defines [pred] COMPUT_1:def 27 :
[pred] = primrec ((0 const 0),(2 proj 1),1);