Rank | Theorem | Name |
5 | Thm* eq:EqDecider(A), P:(A Type Prop), f,g:x:A fp-> Type.
Thm* y dom(f). w=f(y)  P(y,w)
Thm* 
Thm* y dom(g). w=g(y)  P(y,w)  y dom(f g). w=f g(y)  P(y,w) | [fpf-all-join-decl] |
cites the following: |
0 | Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A.
Thm* f g(x) ~ if x dom(f) f(x) else g(x) fi | [fpf-join-ap-sq] |
4 | Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A.
Thm* x dom(f g)  x dom(f) x dom(g) | [fpf-join-dom2] |