:: deftheorem defines [*] COMPUT_1:def 24 :
[*] = primrec ((1 const 0),((1,2)->(1,?,2) [+]),2);