9 lines
138 B
Text
9 lines
138 B
Text
mutual {
|
|
F : Nat -> Nat
|
|
F Z = (S Z)
|
|
F (S n) = (S n) `minus` M(F(n))
|
|
|
|
M : Nat -> Nat
|
|
M Z = Z
|
|
M (S n) = (S n) `minus` F(M(n))
|
|
}
|