2
module TerminationTupledAckermann where
8
data _×_ (A B : Set) : Set where
12
add : Nat × Nat -> Nat
14
add (succ n , m) = succ (add (n , m))
17
ack : Nat × Nat -> Nat
18
ack (zero , y) = succ y
19
ack (succ x , zero) = ack (x , succ zero)
20
ack (succ x , succ y) = ack (x , ack (succ x , y))