1 |
G o g x':A' B'(x') B(g(x'))
 | 2 steps |
2 |
11. G o g x':A' B'(x') B(g(x'))
F o g x':A' B(g(x')) B'(x')
 | 2 steps |
3 |
11. G o g x':A' B'(x') B(g(x'))
12. F o g x':A' B(g(x')) B'(x')
F:(x':A' B'(x') B(g(x'))), G:(x':A' B(g(x')) B'(x')).
InvFuns(A';A;g;f) & ( u:A'. InvFuns(B'(u);B(g(u));F(u);G(u)))
 | 7 steps |