concl,M,N:Formula List, q,r:Formula.
|= < q.(M @ N),concl > 
|= < r.(M @ N),concl > |= < M @ (q
r.N),concl >
formula_or_left_sound
q == inr(inr(inr(inl( < p,q > ))))
Thm* concl,M,N:Formula List, q,r:Formula.
|= < q.(M @ N),concl >
|= < r.(M @ N),concl > |= < M @ (qr.N),concl >
formula_or_left_sound
Thm* 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 >
formula_or_left_falsifiable
Thm* 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 >
formula_or_left_sat
Thm* hyp,M,N:Formula List, q,r:Formula.
|= < hyp,[q; r/ M @ N] > |= < hyp,M @ (qr.N) >
formula_or_right_sound
Thm* hyp,M,N:Formula List, q,r:Formula, a:Assignment.
a | < hyp,[q; r/ M @ N] > a | < hyp,M @ (qr.N) >
formula_or_right_falsifiable
Thm* hyp,M,N:Formula List, q,r:Formula, a:Assignment.
a |= < hyp,[q; r/ M @ N] > a |= < hyp,M @ (qr.N) >
formula_or_right_sat
In prior sections: sat lemmas