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