2. f :
n
3. g :
n
4.
x:. g(f(x)) = x
5.
y:n. f(g(y)) = y
6. (
x.if x=
0
n else f(x-1) fi) 
(n+1)
7. (
y.if y=n 0 else g(y)+1 fi) (n+1)
InvFuns(;(n+1);x.if x=0 n else f(x-1) fi;y.if y=n 0 else g(y)+1 fi)
n
n
x:. g(f(x)) = x
y:n. f(g(y)) = y
x.if x=0 n else f(x-1) fi) (n+1)
y.if y=n 0 else g(y)+1 fi) (n+1)
InvFuns(;(n+1);x.if x=0 n else f(x-1) fi;y.if y=n 0 else g(y)+1 fi)| By: |
THEN Reduce Concl THEN SplitOnNthConclITE Hyp:3 THEN SplitOnConclITE |
| 1 |
9.  x = 0
10. f(x-1) = n
g(f(x-1))+1 = x  | 1 step |
| 2 |
(n+1)
9. y = n
10. g(y)+1 = 0
f(g(y)+1-1) = y (n+1) | 1 step |
About:
 |  |  |  |
 |  |  |  |  |
 |