- model_def
-
|- ∀M. model M ⇔ ∀x. (x,T) ∉ M ∨ (x,F) ∉ M
- models_clause_def
-
|- ∀M c. models_clause M c ⇔ M ∩ c ≠ ∅
- models_formula_def
-
|- ∀M phi. models_formula M phi ⇔ ∀c. c ∈ phi ⇒ models_clause M c
- image_clause_def
-
|- ∀f c. image_clause f c = IMAGE (λl. (f (FST l),SND l)) c
- image_formula_def
-
|- ∀f phi. image_formula f phi = IMAGE (image_clause f) phi
- consistent_tvsal_def
-
|- ∀tvsal phi phi'.
consistent_tvsal (tvsal,phi,phi') ⇔ image_formula tvsal phi ⊆ phi'
- covering_tvsals_def
-
|- ∀tvsals phi phi'.
covering_tvsals (tvsals,phi,phi') ⇔
phi' ⊆ BIGUNION {image_formula tvsal phi | tvsal ∈ tvsals}
- clause_dom_def
-
|- ∀c. clause_dom c = {x | ∃bv. (x,bv) ∈ c}
- formula_dom_def
-
|- ∀phi. formula_dom phi = BIGUNION {clause_dom c | c ∈ phi}
- colouring_def
-
|- ∀P phi.
colouring P phi ⇔
∀p x y.
p ∈ P ∧ x ∈ p ∧ y ∈ p ⇒
(x = y) ∨ ∀c. c ∈ phi ⇒ x ∉ clause_dom c ∨ y ∉ clause_dom c