hyp,M,N:Formula List, q,r:Formula.
|= < q.hyp,r.(M @ N) > 
|= < hyp,M @ (q
r.N) >
formula_imp_right_sound
q == inr(inr(inr(inr( < p,q > ))))
Thm* hyp,M,N:Formula List, q,r:Formula.
|= < q.hyp,r.(M @ N) > |= < hyp,M @ (qr.N) >
formula_imp_right_sound
Thm* hyp,M,N:Formula List, q,r:Formula, a:Assignment.
a |
< q.hyp,r.(M @ N) > 
a | < hyp,M @ (qr.N) >
formula_imp_right_falsifiable
Thm* hyp,M,N:Formula List, q,r:Formula, a:Assignment.
a |= < hyp,M @ (qr.N) > a |= < q.hyp,r.(M @ N) >
formula_imp_right_sat
Thm* concl,M,N:Formula List, q,r:Formula.
|= < M @ N,q.concl >
|= < r.(M @ N),concl > |= < M @ (qr.N),concl >
formula_imp_left_sound
Thm* 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 >
formula_imp_left_falsifiable
Thm* 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 >
formula_imp_left_sat
In prior sections: sat lemmas