Exercise logic.propositional.consequence

Description
Prove that formula is a logical consequence of a set of formulas

Feedback

• onefirst
• allfirsts (3)
• allapplications
• derivation
• microsteps

Environment

initial=TList [TVar "q"]

Path 1

path	[0, 0, 4, 0, 0, 3, 0, 0, 0, 0, 1, 3, 3, 0, 1, 4, 4, 5, 4, 3, 0, 0, 0, 1, 0, 5, 6, 1, 3]
steps	29
major rules	3
active labels	consequence simplify andrules

enter consequence, initial, navigator.down, navigator.down, enter cnf, exit cnf, navigator.up, navigator.up, navigator.downlast, enter cnf, check, enter eliminateimplequiv, logic.propositional.defequiv, exit eliminateimplequiv, check, enter demorgan, navigator.down, navigator.right, navigator.down, logic.propositional.demorganand, navigator.up, navigator.up, exit demorgan, check, enter simplify, navigator.down, navigator.right, enter andrules, logic.propositional.absorpand