Selected Objects

THM	zero_rank_all_vars	L:Sequent List, eqS:{Sequent=}, eqF:{Formula=}. sL.((s) = 0) (hyp,concl:Formula List. < hyp,concl > (eqS) L (z:Formula. z(eqF) hyp z(eqF) concl (v:Var. z = v)))
THM	zero_rank_valid_or_falsifiable	L:Sequent List. sL.((s) = 0) sL.|= s (a:Assignment. sL.a | s)
THM	prop_decide	S:Sequent. |= S (a:Assignment. a | S)
THM	propositional_decidability	S:Sequent. |= S (a:Assignment. a | S)