:: deftheorem defines [+] COMPUT_1:def 23 :
[+] = primrec ((1 proj 1),(3 succ 3),2);