:: deftheorem defines [-] COMPUT_1:def 28 :
[-] = primrec ((1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2);