:: deftheorem defines [!] COMPUT_1:def 25 :
[!] = primrec ((0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1);