Changed terminology. Instead of calling sequents complete we call them full.
Cleaned up the proof of completion.
Proved the canonical model is saturated.