| THM | formula_not_left_sat |  concl,M,N:Formula List. f2:Formula. a:Assignment.
a |= <M @ N, f2::concl>    a |= <M @ (   f2::N), concl> |
| THM | formula_not_left_falsifiable | concl,M,N:Formula List. f2:Formula. a:Assignment.
a | <M @ N, f2::concl> a | <M @ (f2::N), concl> |
| THM | formula_not_left_sound | concl,M,N:Formula List. f2:Formula.
|= <M @ N, f2::concl> |= <M @ (f2::N), concl> |
| THM | formula_not_right_sat | hyp,M,N:Formula List. f:Formula. a:Assignment.
a |= <f::hyp, M @ N> a |= <hyp, M @ (f::N)> |
| THM | formula_not_right_falsifiable | hyp,M,N:Formula List. f2:Formula. a:Assignment.
a | <f2::hyp, M @ N> a | <hyp, M @ (f2::N)> |
| THM | formula_not_right_sound | hyp,M,N:Formula List. f2:Formula.
|= <f2::hyp, M @ N> |= <hyp, M @ (f2::N)> |
| THM | formula_and_left_sat | concl,M,N:Formula List. q,r:Formula. a:Assignment.
a |= <q::r::(M @ N), concl> a |= <M @ (q r::N), concl> |
| THM | formula_and_left_falsifiable | concl,M,N:Formula List. q,r:Formula. a:Assignment.
a | <q::r::(M @ N), concl> a | <M @ (qr::N), concl> |
| THM | formula_and_left_sound | concl,M,N:Formula List. q,r:Formula.
|= <q::r::(M @ N), concl> |= <M @ (qr::N), concl> |
| THM | formula_and_right_sat | hyp,M,N:Formula List. q,r:Formula. a:Assignment.
a |= <hyp, q::(M @ N)> a |= <hyp, r::(M @ N)>
a |= <hyp, M @ (qr::N)> |
| THM | formula_and_right_falsifiable | hyp,M,N:Formula List. q,r:Formula. a:Assignment.
a | <hyp, q::(M @ N)>  a | <hyp, r::(M @ N)>
a | <hyp, M @ (qr::N)> |
| THM | formula_and_right_sound | hyp,M,N:Formula List. q,r:Formula.
|= <hyp, q::(M @ N)>
|= <hyp, r::(M @ N)>
|= <hyp, M @ (qr::N)> |
| THM | formula_or_right_sat | hyp,M,N:Formula List. q,r:Formula. a:Assignment.
a |= <hyp, q::r::(M @ N)> a |= <hyp, M @ (qr::N)> |
| THM | formula_or_right_falsifiable | hyp,M,N:Formula List. q,r:Formula. a:Assignment.
a | <hyp, q::r::(M @ N)> a | <hyp, M @ (qr::N)> |
| THM | formula_or_right_sound | hyp,M,N:Formula List. q,r:Formula.
|= <hyp, q::r::(M @ N)> |= <hyp, M @ (qr::N)> |
| THM | formula_or_left_sat | concl,M,N:Formula List. q,r:Formula. a:Assignment.
a |= <q::(M @ N), concl> a |= <r::(M @ N), concl>
a |= <M @ (qr::N), concl> |
| THM | formula_or_left_falsifiable | concl,M,N:Formula List. q,r:Formula. a:Assignment.
a | <q::(M @ N), concl> a | <r::(M @ N), concl>
a | <M @ (qr::N), concl> |
| THM | formula_or_left_sound | concl,M,N:Formula List. q,r:Formula.
|= <q::(M @ N), concl>
|= <r::(M @ N), concl>
|= <M @ (qr::N), concl> |
| THM | formula_imp_left_sat | concl,M,N:Formula List. q,r:Formula. a:Assignment.
a |= <r::(M @ N), concl> a |= <M @ N, q::concl>
a |= <M @ (qr::N), concl> |
| THM | formula_imp_left_falsifiable | concl,M,N:Formula List. q,r:Formula. a:Assignment.
a | <r::(M @ N), concl> a | <M @ N, q::concl>
a | <M @ (qr::N), concl> |
| THM | formula_imp_left_sound | concl,M,N:Formula List. q,r:Formula.
|= <M @ N, q::concl>
|= <r::(M @ N), concl>
|= <M @ (qr::N), concl> |
| THM | formula_imp_right_sat | hyp,M,N:Formula List. q,r:Formula. a:Assignment.
a |= <hyp, M @ (qr::N)> a |= <q::hyp, r::(M @ N)> |
| THM | formula_imp_right_falsifiable | hyp,M,N:Formula List. q,r:Formula. a:Assignment.
a | <q::hyp, r::(M @ N)> a | <hyp, M @ (qr::N)> |
| THM | formula_imp_right_sound | hyp,M,N:Formula List. q,r:Formula.
|= <q::hyp, r::(M @ N)> |= <hyp, M @ (qr::N)> |