Exercise logic.propositional.consequence

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

Feedback

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

Environment

initial=TList [TCon logic1.implies [TVar "p",TCon logic1.implies [TVar "p",TVar "q"]],TVar "p"]

Path 1

path	[0, 0, 0, 3, 0, 0, 2, 0, 0, 3, 0, 0, 0, 2, 0, 0, 3, 1, 2, 0, 0, 0, 0, 2, 0, 0, 0, 0, 2, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0, 3, 3, 1]
steps	42
major rules	5
active labels	consequence

enter consequence, initial, conj-intro, navigator.down, navigator.down, enter cnf, check, navigator.down, check, enter eliminateimplequiv, logic.propositional.defimpl, exit eliminateimplequiv, navigator.up, check, navigator.down, check, enter eliminateimplequiv, navigator.down, navigator.right, logic.propositional.defimpl, navigator.up, exit eliminateimplequiv, navigator.up, check, navigator.down, check, enter simplify, enter orrules, logic.propositional.idempor, exit orrules, exit simplify, navigator.up, exit cnf, navigator.up, navigator.up, navigator.downlast, enter cnf, exit cnf, navigator.up, navigator.down, navigator.down, fakeabsorption