A,B,C:MsgA.
Thm* A || B
Thm*
Thm* ma-frame-compatible(A; B)
Thm*
Thm* ma-sframe-compatible(A; B)
Thm*
Thm* C || A
Thm*
Thm* ma-frame-compatible(C; A)
Thm*
Thm* ma-sframe-compatible(C; A)
Thm*
Thm* C || B
Thm*
Thm* ma-frame-compatible(C; B)
Thm*
Thm* ma-sframe-compatible(C; B)
Thm*
Thm* C || A
B & ma-frame-compatible(C; A B) & ma-sframe-compatible(C; A B)B1,B2:(A
Type), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a).
Thm* f
f geq:EqDecider(X), f,g:x:X fp-> Type, x:X. f g (f(x)?Void r g(x)?T)eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g f (f(x)?T r g(x)?Top)ds,ds':ltg:Id fp-> Type. ds ds' (State(ds') r State(ds))eq:EqDecider(T), f,g,h:x:T fp-> Type.
Thm* f || g
Thm*
Thm* h || f
Thm*
Thm* h || g
Thm*
Thm* g
h f g & f h f g & h g h f g & h f h f geq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a).
Thm* h || f
h || g h || f gB:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x
dom(f g) 
x dom(f) 
x dom(g)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) fieq:EqDecider(A), f,g:a:A fp-> Top, x:A.
Thm* x
dom(f g) x dom(f) x dom(g)