p is not a tautology. not(p) is not a tautology. and(p, q) is not a tautology. not(not(p)) is not a tautology. implies(or(p, q), and(p, q)) is not a tautology. and(or(p, q), implies(not(p), q)) is not a tautology. implies(or(implies(p, q), implies(r, s)), implies(or(p, q), or(r, s))) is not a tautology. Proof for tautology: implies(p, p): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: implies(p, p) [implies-intro(2)] | -------------------- | -------------------- | | 4: not(p) [assumption(or-elim)] | | -------------------- | | | 5: p [assumption(implies-intro)] | | | 6: bottom [not-elim(4, 5)] | | | 7: p [bottom(6)] | | -------------------- | | 8: implies(p, p) [implies-intro(5-7)] | -------------------- | 9: implies(p, p) [or-elim(1, 2-3, 4-8)] Proof for tautology: or(not(p), p): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(not(p), p) [or-intro(2)] | -------------------- | -------------------- | | 4: not(p) [assumption(or-elim)] | | 5: or(not(p), p) [or-intro(4)] | -------------------- | 6: or(not(p), p) [or-elim(1, 2-3, 4-5)] Proof for tautology: not(and(p, not(p))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: not(not(p)) [not-not-intro(2)] | | 4: or(not(p), not(not(p))) [or-intro(3)] | | 5: not(and(p, not(p))) [deMorgan(4)] | -------------------- | -------------------- | | 6: not(p) [assumption(or-elim)] | | 7: or(not(p), not(not(p))) [or-intro(6)] | | 8: not(and(p, not(p))) [deMorgan(7)] | -------------------- | 9: not(and(p, not(p))) [or-elim(1, 2-5, 6-8)] Proof for tautology: implies(p, not(not(p))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: not(not(p)) [not-not-intro(2)] | | 4: implies(p, not(not(p))) [implies-intro(3)] | -------------------- | -------------------- | | 5: not(p) [assumption(or-elim)] | | -------------------- | | | 6: p [assumption(implies-intro)] | | | 7: bottom [not-elim(5, 6)] | | | 8: not(not(p)) [bottom(7)] | | -------------------- | | 9: implies(p, not(not(p))) [implies-intro(6-8)] | -------------------- | 10: implies(p, not(not(p))) [or-elim(1, 2-4, 5-9)] Proof for tautology: implies(not(not(p)), p): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: implies(not(not(p)), p) [implies-intro(2)] | -------------------- | -------------------- | | 4: not(p) [assumption(or-elim)] | | 5: not(not(not(p))) [not-not-intro(4)] | | -------------------- | | | 6: not(not(p)) [assumption(implies-intro)] | | | 7: bottom [not-elim(5, 6)] | | | 8: p [bottom(7)] | | -------------------- | | 9: implies(not(not(p)), p) [implies-intro(6-8)] | -------------------- | 10: implies(not(not(p)), p) [or-elim(1, 2-3, 4-9)] Proof for tautology: implies(and(p, q), or(p, q)): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(p, q) [or-intro(2)] | | | 6: implies(and(p, q), or(p, q)) [implies-intro(5)] | | -------------------- | | -------------------- | | | 7: not(q) [assumption(or-elim)] | | | 8: or(not(p), not(q)) [or-intro(7)] | | | 9: not(and(p, q)) [deMorgan(8)] | | | -------------------- | | | | 10: and(p, q) [assumption(implies-intro)] | | | | 11: bottom [not-elim(9, 10)] | | | | 12: or(p, q) [bottom(11)] | | | -------------------- | | | 13: implies(and(p, q), or(p, q)) [implies-intro(10-12)] | | -------------------- | | 14: implies(and(p, q), or(p, q)) [or-elim(3, 4-6, 7-13)] | -------------------- | -------------------- | | 15: not(p) [assumption(or-elim)] | | 16: or(q, not(q)) [lem] | | -------------------- | | | 17: q [assumption(or-elim)] | | | 18: or(not(p), not(q)) [or-intro(15)] | | | 19: not(and(p, q)) [deMorgan(18)] | | | -------------------- | | | | 20: and(p, q) [assumption(implies-intro)] | | | | 21: bottom [not-elim(19, 20)] | | | | 22: or(p, q) [bottom(21)] | | | -------------------- | | | 23: implies(and(p, q), or(p, q)) [implies-intro(20-22)] | | -------------------- | | -------------------- | | | 24: not(q) [assumption(or-elim)] | | | 25: or(not(p), not(q)) [or-intro(15)] | | | 26: not(and(p, q)) [deMorgan(25)] | | | -------------------- | | | | 27: and(p, q) [assumption(implies-intro)] | | | | 28: bottom [not-elim(26, 27)] | | | | 29: or(p, q) [bottom(28)] | | | -------------------- | | | 30: implies(and(p, q), or(p, q)) [implies-intro(27-29)] | | -------------------- | | 31: implies(and(p, q), or(p, q)) [or-elim(16, 17-23, 24-30)] | -------------------- | 32: implies(and(p, q), or(p, q)) [or-elim(1, 2-14, 15-31)] Proof for tautology: implies(and(p, q), and(q, p)): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: and(q, p) [and-intro(4, 2)] | | | 6: implies(and(p, q), and(q, p)) [implies-intro(5)] | | -------------------- | | -------------------- | | | 7: not(q) [assumption(or-elim)] | | | 8: or(not(p), not(q)) [or-intro(7)] | | | 9: not(and(p, q)) [deMorgan(8)] | | | -------------------- | | | | 10: and(p, q) [assumption(implies-intro)] | | | | 11: bottom [not-elim(9, 10)] | | | | 12: and(q, p) [bottom(11)] | | | -------------------- | | | 13: implies(and(p, q), and(q, p)) [implies-intro(10-12)] | | -------------------- | | 14: implies(and(p, q), and(q, p)) [or-elim(3, 4-6, 7-13)] | -------------------- | -------------------- | | 15: not(p) [assumption(or-elim)] | | 16: or(q, not(q)) [lem] | | -------------------- | | | 17: q [assumption(or-elim)] | | | 18: or(not(p), not(q)) [or-intro(15)] | | | 19: not(and(p, q)) [deMorgan(18)] | | | -------------------- | | | | 20: and(p, q) [assumption(implies-intro)] | | | | 21: bottom [not-elim(19, 20)] | | | | 22: and(q, p) [bottom(21)] | | | -------------------- | | | 23: implies(and(p, q), and(q, p)) [implies-intro(20-22)] | | -------------------- | | -------------------- | | | 24: not(q) [assumption(or-elim)] | | | 25: or(not(p), not(q)) [or-intro(15)] | | | 26: not(and(p, q)) [deMorgan(25)] | | | -------------------- | | | | 27: and(p, q) [assumption(implies-intro)] | | | | 28: bottom [not-elim(26, 27)] | | | | 29: and(q, p) [bottom(28)] | | | -------------------- | | | 30: implies(and(p, q), and(q, p)) [implies-intro(27-29)] | | -------------------- | | 31: implies(and(p, q), and(q, p)) [or-elim(16, 17-23, 24-30)] | -------------------- | 32: implies(and(p, q), and(q, p)) [or-elim(1, 2-14, 15-31)] Proof for tautology: implies(p, implies(not(p), p)): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: not(not(p)) [not-not-intro(2)] | | -------------------- | | | 4: not(p) [assumption(implies-intro)] | | | 5: bottom [not-elim(3, 4)] | | | 6: p [bottom(5)] | | -------------------- | | 7: implies(not(p), p) [implies-intro(4-6)] | | 8: implies(p, implies(not(p), p)) [implies-intro(7)] | -------------------- | -------------------- | | 9: not(p) [assumption(or-elim)] | | -------------------- | | | 10: p [assumption(implies-intro)] | | | 11: bottom [not-elim(9, 10)] | | | 12: implies(not(p), p) [bottom(11)] | | -------------------- | | 13: implies(p, implies(not(p), p)) [implies-intro(10-12)] | -------------------- | 14: implies(p, implies(not(p), p)) [or-elim(1, 2-8, 9-13)] Proof for tautology: implies(implies(p, q), implies(not(q), not(p))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: not(not(q)) [not-not-intro(4)] | | | -------------------- | | | | 6: not(q) [assumption(implies-intro)] | | | | 7: bottom [not-elim(5, 6)] | | | | 8: not(p) [bottom(7)] | | | -------------------- | | | 9: implies(not(q), not(p)) [implies-intro(6-8)] | | | 10: implies(implies(p, q), implies(not(q), not(p))) [implies-intro(9)] | | -------------------- | | -------------------- | | | 11: not(q) [assumption(or-elim)] | | | -------------------- | | | | 12: implies(p, q) [assumption(not-intro)] | | | | 13: q [implies-elim(2, 12)] | | | | 14: bottom [not-elim(11, 13)] | | | -------------------- | | | 15: not(implies(p, q)) [not-intro(12-14)] | | | -------------------- | | | | 16: implies(p, q) [assumption(implies-intro)] | | | | 17: bottom [not-elim(15, 16)] | | | | 18: implies(not(q), not(p)) [bottom(17)] | | | -------------------- | | | 19: implies(implies(p, q), implies(not(q), not(p))) [implies-intro(16-18)] | | -------------------- | | 20: implies(implies(p, q), implies(not(q), not(p))) [or-elim(3, 4-10, 11-19)] | -------------------- | -------------------- | | 21: not(p) [assumption(or-elim)] | | 22: or(q, not(q)) [lem] | | -------------------- | | | 23: q [assumption(or-elim)] | | | 24: not(not(q)) [not-not-intro(23)] | | | -------------------- | | | | 25: not(q) [assumption(implies-intro)] | | | | 26: bottom [not-elim(24, 25)] | | | | 27: not(p) [bottom(26)] | | | -------------------- | | | 28: implies(not(q), not(p)) [implies-intro(25-27)] | | | 29: implies(implies(p, q), implies(not(q), not(p))) [implies-intro(28)] | | -------------------- | | -------------------- | | | 30: not(q) [assumption(or-elim)] | | | 31: implies(not(q), not(p)) [implies-intro(21)] | | | 32: implies(implies(p, q), implies(not(q), not(p))) [implies-intro(31)] | | -------------------- | | 33: implies(implies(p, q), implies(not(q), not(p))) [or-elim(22, 23-29, 30-32)] | -------------------- | 34: implies(implies(p, q), implies(not(q), not(p))) [or-elim(1, 2-20, 21-33)] Proof for tautology: implies(implies(not(q), not(p)), implies(p, q)): | 1: or(q, not(q)) [lem] | -------------------- | | 2: q [assumption(or-elim)] | | 3: or(p, not(p)) [lem] | | -------------------- | | | 4: p [assumption(or-elim)] | | | 5: implies(p, q) [implies-intro(2)] | | | 6: implies(implies(not(q), not(p)), implies(p, q)) [implies-intro(5)] | | -------------------- | | -------------------- | | | 7: not(p) [assumption(or-elim)] | | | -------------------- | | | | 8: p [assumption(implies-intro)] | | | | 9: bottom [not-elim(7, 8)] | | | | 10: q [bottom(9)] | | | -------------------- | | | 11: implies(p, q) [implies-intro(8-10)] | | | 12: implies(implies(not(q), not(p)), implies(p, q)) [implies-intro(11)] | | -------------------- | | 13: implies(implies(not(q), not(p)), implies(p, q)) [or-elim(3, 4-6, 7-12)] | -------------------- | -------------------- | | 14: not(q) [assumption(or-elim)] | | 15: or(p, not(p)) [lem] | | -------------------- | | | 16: p [assumption(or-elim)] | | | 17: not(not(p)) [not-not-intro(16)] | | | -------------------- | | | | 18: implies(not(q), not(p)) [assumption(not-intro)] | | | | 19: not(p) [implies-elim(14, 18)] | | | | 20: bottom [not-elim(17, 19)] | | | -------------------- | | | 21: not(implies(not(q), not(p))) [not-intro(18-20)] | | | -------------------- | | | | 22: implies(not(q), not(p)) [assumption(implies-intro)] | | | | 23: bottom [not-elim(21, 22)] | | | | 24: implies(p, q) [bottom(23)] | | | -------------------- | | | 25: implies(implies(not(q), not(p)), implies(p, q)) [implies-intro(22-24)] | | -------------------- | | -------------------- | | | 26: not(p) [assumption(or-elim)] | | | -------------------- | | | | 27: p [assumption(implies-intro)] | | | | 28: bottom [not-elim(26, 27)] | | | | 29: q [bottom(28)] | | | -------------------- | | | 30: implies(p, q) [implies-intro(27-29)] | | | 31: implies(implies(not(q), not(p)), implies(p, q)) [implies-intro(30)] | | -------------------- | | 32: implies(implies(not(q), not(p)), implies(p, q)) [or-elim(15, 16-25, 26-31)] | -------------------- | 33: implies(implies(not(q), not(p)), implies(p, q)) [or-elim(1, 2-13, 14-32)] Proof for tautology: implies(implies(p, implies(q, r)), implies(and(p, q), r)): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: implies(and(p, q), r) [implies-intro(6)] | | | | 8: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(7)] | | | -------------------- | | | -------------------- | | | | 9: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 10: implies(q, r) [assumption(not-intro)] | | | | | 11: r [implies-elim(4, 10)] | | | | | 12: bottom [not-elim(9, 11)] | | | | -------------------- | | | | 13: not(implies(q, r)) [not-intro(10-12)] | | | | -------------------- | | | | | 14: implies(p, implies(q, r)) [assumption(not-intro)] | | | | | 15: implies(q, r) [implies-elim(2, 14)] | | | | | 16: bottom [not-elim(13, 15)] | | | | -------------------- | | | | 17: not(implies(p, implies(q, r))) [not-intro(14-16)] | | | | -------------------- | | | | | 18: implies(p, implies(q, r)) [assumption(implies-intro)] | | | | | 19: bottom [not-elim(17, 18)] | | | | | 20: implies(and(p, q), r) [bottom(19)] | | | | -------------------- | | | | 21: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(18-20)] | | | -------------------- | | | 22: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [or-elim(5, 6-8, 9-21)] | | -------------------- | | -------------------- | | | 23: not(q) [assumption(or-elim)] | | | 24: or(r, not(r)) [lem] | | | -------------------- | | | | 25: r [assumption(or-elim)] | | | | 26: or(not(p), not(q)) [or-intro(23)] | | | | 27: not(and(p, q)) [deMorgan(26)] | | | | -------------------- | | | | | 28: and(p, q) [assumption(implies-intro)] | | | | | 29: bottom [not-elim(27, 28)] | | | | | 30: r [bottom(29)] | | | | -------------------- | | | | 31: implies(and(p, q), r) [implies-intro(28-30)] | | | | 32: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(31)] | | | -------------------- | | | -------------------- | | | | 33: not(r) [assumption(or-elim)] | | | | 34: or(not(p), not(q)) [or-intro(23)] | | | | 35: not(and(p, q)) [deMorgan(34)] | | | | -------------------- | | | | | 36: and(p, q) [assumption(implies-intro)] | | | | | 37: bottom [not-elim(35, 36)] | | | | | 38: r [bottom(37)] | | | | -------------------- | | | | 39: implies(and(p, q), r) [implies-intro(36-38)] | | | | 40: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(39)] | | | -------------------- | | | 41: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [or-elim(24, 25-32, 33-40)] | | -------------------- | | 42: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [or-elim(3, 4-22, 23-41)] | -------------------- | -------------------- | | 43: not(p) [assumption(or-elim)] | | 44: or(q, not(q)) [lem] | | -------------------- | | | 45: q [assumption(or-elim)] | | | 46: or(r, not(r)) [lem] | | | -------------------- | | | | 47: r [assumption(or-elim)] | | | | 48: or(not(p), not(q)) [or-intro(43)] | | | | 49: not(and(p, q)) [deMorgan(48)] | | | | -------------------- | | | | | 50: and(p, q) [assumption(implies-intro)] | | | | | 51: bottom [not-elim(49, 50)] | | | | | 52: r [bottom(51)] | | | | -------------------- | | | | 53: implies(and(p, q), r) [implies-intro(50-52)] | | | | 54: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(53)] | | | -------------------- | | | -------------------- | | | | 55: not(r) [assumption(or-elim)] | | | | 56: or(not(p), not(q)) [or-intro(43)] | | | | 57: not(and(p, q)) [deMorgan(56)] | | | | -------------------- | | | | | 58: and(p, q) [assumption(implies-intro)] | | | | | 59: bottom [not-elim(57, 58)] | | | | | 60: r [bottom(59)] | | | | -------------------- | | | | 61: implies(and(p, q), r) [implies-intro(58-60)] | | | | 62: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(61)] | | | -------------------- | | | 63: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [or-elim(46, 47-54, 55-62)] | | -------------------- | | -------------------- | | | 64: not(q) [assumption(or-elim)] | | | 65: or(r, not(r)) [lem] | | | -------------------- | | | | 66: r [assumption(or-elim)] | | | | 67: or(not(p), not(q)) [or-intro(43)] | | | | 68: not(and(p, q)) [deMorgan(67)] | | | | -------------------- | | | | | 69: and(p, q) [assumption(implies-intro)] | | | | | 70: bottom [not-elim(68, 69)] | | | | | 71: r [bottom(70)] | | | | -------------------- | | | | 72: implies(and(p, q), r) [implies-intro(69-71)] | | | | 73: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(72)] | | | -------------------- | | | -------------------- | | | | 74: not(r) [assumption(or-elim)] | | | | 75: or(not(p), not(q)) [or-intro(43)] | | | | 76: not(and(p, q)) [deMorgan(75)] | | | | -------------------- | | | | | 77: and(p, q) [assumption(implies-intro)] | | | | | 78: bottom [not-elim(76, 77)] | | | | | 79: r [bottom(78)] | | | | -------------------- | | | | 80: implies(and(p, q), r) [implies-intro(77-79)] | | | | 81: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [implies-intro(80)] | | | -------------------- | | | 82: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [or-elim(65, 66-73, 74-81)] | | -------------------- | | 83: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [or-elim(44, 45-63, 64-82)] | -------------------- | 84: implies(implies(p, implies(q, r)), implies(and(p, q), r)) [or-elim(1, 2-42, 43-83)] Proof for tautology: implies(not(and(p, q)), or(not(p), not(q))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: and(p, q) [and-intro(2, 4)] | | | 6: not(not(and(p, q))) [not-not-intro(5)] | | | -------------------- | | | | 7: not(and(p, q)) [assumption(implies-intro)] | | | | 8: bottom [not-elim(6, 7)] | | | | 9: or(not(p), not(q)) [bottom(8)] | | | -------------------- | | | 10: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(7-9)] | | -------------------- | | -------------------- | | | 11: not(q) [assumption(or-elim)] | | | 12: or(not(p), not(q)) [or-intro(11)] | | | 13: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(12)] | | -------------------- | | 14: implies(not(and(p, q)), or(not(p), not(q))) [or-elim(3, 4-10, 11-13)] | -------------------- | -------------------- | | 15: not(p) [assumption(or-elim)] | | 16: or(q, not(q)) [lem] | | -------------------- | | | 17: q [assumption(or-elim)] | | | 18: or(not(p), not(q)) [or-intro(15)] | | | 19: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(18)] | | -------------------- | | -------------------- | | | 20: not(q) [assumption(or-elim)] | | | 21: or(not(p), not(q)) [or-intro(15)] | | | 22: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(21)] | | -------------------- | | 23: implies(not(and(p, q)), or(not(p), not(q))) [or-elim(16, 17-19, 20-22)] | -------------------- | 24: implies(not(and(p, q)), or(not(p), not(q))) [or-elim(1, 2-14, 15-23)] Proof for tautology: implies(implies(and(p, q), r), implies(p, implies(q, r))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: implies(q, r) [implies-intro(6)] | | | | 8: implies(p, implies(q, r)) [implies-intro(7)] | | | | 9: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(8)] | | | -------------------- | | | -------------------- | | | | 10: not(r) [assumption(or-elim)] | | | | 11: and(p, q) [and-intro(2, 4)] | | | | -------------------- | | | | | 12: implies(and(p, q), r) [assumption(not-intro)] | | | | | 13: r [implies-elim(11, 12)] | | | | | 14: bottom [not-elim(10, 13)] | | | | -------------------- | | | | 15: not(implies(and(p, q), r)) [not-intro(12-14)] | | | | -------------------- | | | | | 16: implies(and(p, q), r) [assumption(implies-intro)] | | | | | 17: bottom [not-elim(15, 16)] | | | | | 18: implies(p, implies(q, r)) [bottom(17)] | | | | -------------------- | | | | 19: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(16-18)] | | | -------------------- | | | 20: implies(implies(and(p, q), r), implies(p, implies(q, r))) [or-elim(5, 6-9, 10-19)] | | -------------------- | | -------------------- | | | 21: not(q) [assumption(or-elim)] | | | 22: or(r, not(r)) [lem] | | | -------------------- | | | | 23: r [assumption(or-elim)] | | | | -------------------- | | | | | 24: q [assumption(implies-intro)] | | | | | 25: bottom [not-elim(21, 24)] | | | | | 26: r [bottom(25)] | | | | -------------------- | | | | 27: implies(q, r) [implies-intro(24-26)] | | | | 28: implies(p, implies(q, r)) [implies-intro(27)] | | | | 29: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(28)] | | | -------------------- | | | -------------------- | | | | 30: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 31: q [assumption(implies-intro)] | | | | | 32: bottom [not-elim(21, 31)] | | | | | 33: r [bottom(32)] | | | | -------------------- | | | | 34: implies(q, r) [implies-intro(31-33)] | | | | 35: implies(p, implies(q, r)) [implies-intro(34)] | | | | 36: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(35)] | | | -------------------- | | | 37: implies(implies(and(p, q), r), implies(p, implies(q, r))) [or-elim(22, 23-29, 30-36)] | | -------------------- | | 38: implies(implies(and(p, q), r), implies(p, implies(q, r))) [or-elim(3, 4-20, 21-37)] | -------------------- | -------------------- | | 39: not(p) [assumption(or-elim)] | | 40: or(q, not(q)) [lem] | | -------------------- | | | 41: q [assumption(or-elim)] | | | 42: or(r, not(r)) [lem] | | | -------------------- | | | | 43: r [assumption(or-elim)] | | | | -------------------- | | | | | 44: p [assumption(implies-intro)] | | | | | 45: bottom [not-elim(39, 44)] | | | | | 46: implies(q, r) [bottom(45)] | | | | -------------------- | | | | 47: implies(p, implies(q, r)) [implies-intro(44-46)] | | | | 48: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(47)] | | | -------------------- | | | -------------------- | | | | 49: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 50: p [assumption(implies-intro)] | | | | | 51: bottom [not-elim(39, 50)] | | | | | 52: implies(q, r) [bottom(51)] | | | | -------------------- | | | | 53: implies(p, implies(q, r)) [implies-intro(50-52)] | | | | 54: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(53)] | | | -------------------- | | | 55: implies(implies(and(p, q), r), implies(p, implies(q, r))) [or-elim(42, 43-48, 49-54)] | | -------------------- | | -------------------- | | | 56: not(q) [assumption(or-elim)] | | | 57: or(r, not(r)) [lem] | | | -------------------- | | | | 58: r [assumption(or-elim)] | | | | -------------------- | | | | | 59: p [assumption(implies-intro)] | | | | | 60: bottom [not-elim(39, 59)] | | | | | 61: implies(q, r) [bottom(60)] | | | | -------------------- | | | | 62: implies(p, implies(q, r)) [implies-intro(59-61)] | | | | 63: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(62)] | | | -------------------- | | | -------------------- | | | | 64: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 65: p [assumption(implies-intro)] | | | | | 66: bottom [not-elim(39, 65)] | | | | | 67: implies(q, r) [bottom(66)] | | | | -------------------- | | | | 68: implies(p, implies(q, r)) [implies-intro(65-67)] | | | | 69: implies(implies(and(p, q), r), implies(p, implies(q, r))) [implies-intro(68)] | | | -------------------- | | | 70: implies(implies(and(p, q), r), implies(p, implies(q, r))) [or-elim(57, 58-63, 64-69)] | | -------------------- | | 71: implies(implies(and(p, q), r), implies(p, implies(q, r))) [or-elim(40, 41-55, 56-70)] | -------------------- | 72: implies(implies(and(p, q), r), implies(p, implies(q, r))) [or-elim(1, 2-38, 39-71)] Proof for tautology: implies(implies(and(p, q), r), implies(q, implies(p, r))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: implies(p, r) [implies-intro(6)] | | | | 8: implies(q, implies(p, r)) [implies-intro(7)] | | | | 9: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(8)] | | | -------------------- | | | -------------------- | | | | 10: not(r) [assumption(or-elim)] | | | | 11: and(p, q) [and-intro(2, 4)] | | | | -------------------- | | | | | 12: implies(and(p, q), r) [assumption(not-intro)] | | | | | 13: r [implies-elim(11, 12)] | | | | | 14: bottom [not-elim(10, 13)] | | | | -------------------- | | | | 15: not(implies(and(p, q), r)) [not-intro(12-14)] | | | | -------------------- | | | | | 16: implies(and(p, q), r) [assumption(implies-intro)] | | | | | 17: bottom [not-elim(15, 16)] | | | | | 18: implies(q, implies(p, r)) [bottom(17)] | | | | -------------------- | | | | 19: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(16-18)] | | | -------------------- | | | 20: implies(implies(and(p, q), r), implies(q, implies(p, r))) [or-elim(5, 6-9, 10-19)] | | -------------------- | | -------------------- | | | 21: not(q) [assumption(or-elim)] | | | 22: or(r, not(r)) [lem] | | | -------------------- | | | | 23: r [assumption(or-elim)] | | | | -------------------- | | | | | 24: q [assumption(implies-intro)] | | | | | 25: bottom [not-elim(21, 24)] | | | | | 26: implies(p, r) [bottom(25)] | | | | -------------------- | | | | 27: implies(q, implies(p, r)) [implies-intro(24-26)] | | | | 28: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(27)] | | | -------------------- | | | -------------------- | | | | 29: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 30: q [assumption(implies-intro)] | | | | | 31: bottom [not-elim(21, 30)] | | | | | 32: implies(p, r) [bottom(31)] | | | | -------------------- | | | | 33: implies(q, implies(p, r)) [implies-intro(30-32)] | | | | 34: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(33)] | | | -------------------- | | | 35: implies(implies(and(p, q), r), implies(q, implies(p, r))) [or-elim(22, 23-28, 29-34)] | | -------------------- | | 36: implies(implies(and(p, q), r), implies(q, implies(p, r))) [or-elim(3, 4-20, 21-35)] | -------------------- | -------------------- | | 37: not(p) [assumption(or-elim)] | | 38: or(q, not(q)) [lem] | | -------------------- | | | 39: q [assumption(or-elim)] | | | 40: or(r, not(r)) [lem] | | | -------------------- | | | | 41: r [assumption(or-elim)] | | | | -------------------- | | | | | 42: p [assumption(implies-intro)] | | | | | 43: bottom [not-elim(37, 42)] | | | | | 44: r [bottom(43)] | | | | -------------------- | | | | 45: implies(p, r) [implies-intro(42-44)] | | | | 46: implies(q, implies(p, r)) [implies-intro(45)] | | | | 47: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(46)] | | | -------------------- | | | -------------------- | | | | 48: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 49: p [assumption(implies-intro)] | | | | | 50: bottom [not-elim(37, 49)] | | | | | 51: r [bottom(50)] | | | | -------------------- | | | | 52: implies(p, r) [implies-intro(49-51)] | | | | 53: implies(q, implies(p, r)) [implies-intro(52)] | | | | 54: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(53)] | | | -------------------- | | | 55: implies(implies(and(p, q), r), implies(q, implies(p, r))) [or-elim(40, 41-47, 48-54)] | | -------------------- | | -------------------- | | | 56: not(q) [assumption(or-elim)] | | | 57: or(r, not(r)) [lem] | | | -------------------- | | | | 58: r [assumption(or-elim)] | | | | -------------------- | | | | | 59: q [assumption(implies-intro)] | | | | | 60: bottom [not-elim(56, 59)] | | | | | 61: implies(p, r) [bottom(60)] | | | | -------------------- | | | | 62: implies(q, implies(p, r)) [implies-intro(59-61)] | | | | 63: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(62)] | | | -------------------- | | | -------------------- | | | | 64: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 65: q [assumption(implies-intro)] | | | | | 66: bottom [not-elim(56, 65)] | | | | | 67: implies(p, r) [bottom(66)] | | | | -------------------- | | | | 68: implies(q, implies(p, r)) [implies-intro(65-67)] | | | | 69: implies(implies(and(p, q), r), implies(q, implies(p, r))) [implies-intro(68)] | | | -------------------- | | | 70: implies(implies(and(p, q), r), implies(q, implies(p, r))) [or-elim(57, 58-63, 64-69)] | | -------------------- | | 71: implies(implies(and(p, q), r), implies(q, implies(p, r))) [or-elim(38, 39-55, 56-70)] | -------------------- | 72: implies(implies(and(p, q), r), implies(q, implies(p, r))) [or-elim(1, 2-36, 37-71)] Proof for tautology: or(implies(p, q), implies(q, r)): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: implies(p, q) [implies-intro(4)] | | | | 8: or(implies(p, q), implies(q, r)) [or-intro(7)] | | | -------------------- | | | -------------------- | | | | 9: not(r) [assumption(or-elim)] | | | | 10: implies(p, q) [implies-intro(4)] | | | | 11: or(implies(p, q), implies(q, r)) [or-intro(10)] | | | -------------------- | | | 12: or(implies(p, q), implies(q, r)) [or-elim(5, 6-8, 9-11)] | | -------------------- | | -------------------- | | | 13: not(q) [assumption(or-elim)] | | | 14: or(r, not(r)) [lem] | | | -------------------- | | | | 15: r [assumption(or-elim)] | | | | -------------------- | | | | | 16: q [assumption(implies-intro)] | | | | | 17: bottom [not-elim(13, 16)] | | | | | 18: r [bottom(17)] | | | | -------------------- | | | | 19: implies(q, r) [implies-intro(16-18)] | | | | 20: or(implies(p, q), implies(q, r)) [or-intro(19)] | | | -------------------- | | | -------------------- | | | | 21: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 22: q [assumption(implies-intro)] | | | | | 23: bottom [not-elim(13, 22)] | | | | | 24: r [bottom(23)] | | | | -------------------- | | | | 25: implies(q, r) [implies-intro(22-24)] | | | | 26: or(implies(p, q), implies(q, r)) [or-intro(25)] | | | -------------------- | | | 27: or(implies(p, q), implies(q, r)) [or-elim(14, 15-20, 21-26)] | | -------------------- | | 28: or(implies(p, q), implies(q, r)) [or-elim(3, 4-12, 13-27)] | -------------------- | -------------------- | | 29: not(p) [assumption(or-elim)] | | 30: or(q, not(q)) [lem] | | -------------------- | | | 31: q [assumption(or-elim)] | | | 32: or(r, not(r)) [lem] | | | -------------------- | | | | 33: r [assumption(or-elim)] | | | | -------------------- | | | | | 34: p [assumption(implies-intro)] | | | | | 35: bottom [not-elim(29, 34)] | | | | | 36: q [bottom(35)] | | | | -------------------- | | | | 37: implies(p, q) [implies-intro(34-36)] | | | | 38: or(implies(p, q), implies(q, r)) [or-intro(37)] | | | -------------------- | | | -------------------- | | | | 39: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 40: p [assumption(implies-intro)] | | | | | 41: bottom [not-elim(29, 40)] | | | | | 42: q [bottom(41)] | | | | -------------------- | | | | 43: implies(p, q) [implies-intro(40-42)] | | | | 44: or(implies(p, q), implies(q, r)) [or-intro(43)] | | | -------------------- | | | 45: or(implies(p, q), implies(q, r)) [or-elim(32, 33-38, 39-44)] | | -------------------- | | -------------------- | | | 46: not(q) [assumption(or-elim)] | | | 47: or(r, not(r)) [lem] | | | -------------------- | | | | 48: r [assumption(or-elim)] | | | | -------------------- | | | | | 49: p [assumption(implies-intro)] | | | | | 50: bottom [not-elim(29, 49)] | | | | | 51: q [bottom(50)] | | | | -------------------- | | | | 52: implies(p, q) [implies-intro(49-51)] | | | | 53: or(implies(p, q), implies(q, r)) [or-intro(52)] | | | -------------------- | | | -------------------- | | | | 54: not(r) [assumption(or-elim)] | | | | -------------------- | | | | | 55: p [assumption(implies-intro)] | | | | | 56: bottom [not-elim(29, 55)] | | | | | 57: q [bottom(56)] | | | | -------------------- | | | | 58: implies(p, q) [implies-intro(55-57)] | | | | 59: or(implies(p, q), implies(q, r)) [or-intro(58)] | | | -------------------- | | | 60: or(implies(p, q), implies(q, r)) [or-elim(47, 48-53, 54-59)] | | -------------------- | | 61: or(implies(p, q), implies(q, r)) [or-elim(30, 31-45, 46-60)] | -------------------- | 62: or(implies(p, q), implies(q, r)) [or-elim(1, 2-28, 29-61)] Proof for tautology: implies(or(p, q), or(p, and(q, not(p)))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(p, and(q, not(p))) [or-intro(2)] | | | 6: implies(or(p, q), or(p, and(q, not(p)))) [implies-intro(5)] | | -------------------- | | -------------------- | | | 7: not(q) [assumption(or-elim)] | | | 8: or(p, and(q, not(p))) [or-intro(2)] | | | 9: implies(or(p, q), or(p, and(q, not(p)))) [implies-intro(8)] | | -------------------- | | 10: implies(or(p, q), or(p, and(q, not(p)))) [or-elim(3, 4-6, 7-9)] | -------------------- | -------------------- | | 11: not(p) [assumption(or-elim)] | | 12: or(q, not(q)) [lem] | | -------------------- | | | 13: q [assumption(or-elim)] | | | 14: and(q, not(p)) [and-intro(13, 11)] | | | 15: or(p, and(q, not(p))) [or-intro(14)] | | | 16: implies(or(p, q), or(p, and(q, not(p)))) [implies-intro(15)] | | -------------------- | | -------------------- | | | 17: not(q) [assumption(or-elim)] | | | 18: and(not(p), not(q)) [and-intro(11, 17)] | | | 19: not(or(p, q)) [deMorgan(18)] | | | -------------------- | | | | 20: or(p, q) [assumption(implies-intro)] | | | | 21: bottom [not-elim(19, 20)] | | | | 22: or(p, and(q, not(p))) [bottom(21)] | | | -------------------- | | | 23: implies(or(p, q), or(p, and(q, not(p)))) [implies-intro(20-22)] | | -------------------- | | 24: implies(or(p, q), or(p, and(q, not(p)))) [or-elim(12, 13-16, 17-23)] | -------------------- | 25: implies(or(p, q), or(p, and(q, not(p)))) [or-elim(1, 2-10, 11-24)] Proof for tautology: implies(or(p, and(q, not(p))), or(p, q)): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(p, q) [or-intro(2)] | | | 6: implies(or(p, and(q, not(p))), or(p, q)) [implies-intro(5)] | | -------------------- | | -------------------- | | | 7: not(q) [assumption(or-elim)] | | | 8: or(p, q) [or-intro(2)] | | | 9: implies(or(p, and(q, not(p))), or(p, q)) [implies-intro(8)] | | -------------------- | | 10: implies(or(p, and(q, not(p))), or(p, q)) [or-elim(3, 4-6, 7-9)] | -------------------- | -------------------- | | 11: not(p) [assumption(or-elim)] | | 12: or(q, not(q)) [lem] | | -------------------- | | | 13: q [assumption(or-elim)] | | | 14: or(p, q) [or-intro(13)] | | | 15: implies(or(p, and(q, not(p))), or(p, q)) [implies-intro(14)] | | -------------------- | | -------------------- | | | 16: not(q) [assumption(or-elim)] | | | 17: or(not(q), not(not(p))) [or-intro(16)] | | | 18: not(and(q, not(p))) [deMorgan(17)] | | | 19: and(not(p), not(and(q, not(p)))) [and-intro(11, 18)] | | | 20: not(or(p, and(q, not(p)))) [deMorgan(19)] | | | -------------------- | | | | 21: or(p, and(q, not(p))) [assumption(implies-intro)] | | | | 22: bottom [not-elim(20, 21)] | | | | 23: or(p, q) [bottom(22)] | | | -------------------- | | | 24: implies(or(p, and(q, not(p))), or(p, q)) [implies-intro(21-23)] | | -------------------- | | 25: implies(or(p, and(q, not(p))), or(p, q)) [or-elim(12, 13-15, 16-24)] | -------------------- | 26: implies(or(p, and(q, not(p))), or(p, q)) [or-elim(1, 2-10, 11-25)] Proof for tautology: implies(not(and(p, q)), or(not(p), not(q))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: and(p, q) [and-intro(2, 4)] | | | 6: not(not(and(p, q))) [not-not-intro(5)] | | | -------------------- | | | | 7: not(and(p, q)) [assumption(implies-intro)] | | | | 8: bottom [not-elim(6, 7)] | | | | 9: or(not(p), not(q)) [bottom(8)] | | | -------------------- | | | 10: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(7-9)] | | -------------------- | | -------------------- | | | 11: not(q) [assumption(or-elim)] | | | 12: or(not(p), not(q)) [or-intro(11)] | | | 13: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(12)] | | -------------------- | | 14: implies(not(and(p, q)), or(not(p), not(q))) [or-elim(3, 4-10, 11-13)] | -------------------- | -------------------- | | 15: not(p) [assumption(or-elim)] | | 16: or(q, not(q)) [lem] | | -------------------- | | | 17: q [assumption(or-elim)] | | | 18: or(not(p), not(q)) [or-intro(15)] | | | 19: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(18)] | | -------------------- | | -------------------- | | | 20: not(q) [assumption(or-elim)] | | | 21: or(not(p), not(q)) [or-intro(15)] | | | 22: implies(not(and(p, q)), or(not(p), not(q))) [implies-intro(21)] | | -------------------- | | 23: implies(not(and(p, q)), or(not(p), not(q))) [or-elim(16, 17-19, 20-22)] | -------------------- | 24: implies(not(and(p, q)), or(not(p), not(q))) [or-elim(1, 2-14, 15-23)] Proof for tautology: implies(or(not(p), not(q)), not(and(p, q))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: not(not(p)) [not-not-intro(2)] | | | 6: not(not(q)) [not-not-intro(4)] | | | 7: and(not(not(p)), not(not(q))) [and-intro(5, 6)] | | | 8: not(or(not(p), not(q))) [deMorgan(7)] | | | -------------------- | | | | 9: or(not(p), not(q)) [assumption(implies-intro)] | | | | 10: bottom [not-elim(8, 9)] | | | | 11: not(and(p, q)) [bottom(10)] | | | -------------------- | | | 12: implies(or(not(p), not(q)), not(and(p, q))) [implies-intro(9-11)] | | -------------------- | | -------------------- | | | 13: not(q) [assumption(or-elim)] | | | 14: or(not(p), not(q)) [or-intro(13)] | | | 15: not(and(p, q)) [deMorgan(14)] | | | 16: implies(or(not(p), not(q)), not(and(p, q))) [implies-intro(15)] | | -------------------- | | 17: implies(or(not(p), not(q)), not(and(p, q))) [or-elim(3, 4-12, 13-16)] | -------------------- | -------------------- | | 18: not(p) [assumption(or-elim)] | | 19: or(q, not(q)) [lem] | | -------------------- | | | 20: q [assumption(or-elim)] | | | 21: or(not(p), not(q)) [or-intro(18)] | | | 22: not(and(p, q)) [deMorgan(21)] | | | 23: implies(or(not(p), not(q)), not(and(p, q))) [implies-intro(22)] | | -------------------- | | -------------------- | | | 24: not(q) [assumption(or-elim)] | | | 25: or(not(p), not(q)) [or-intro(18)] | | | 26: not(and(p, q)) [deMorgan(25)] | | | 27: implies(or(not(p), not(q)), not(and(p, q))) [implies-intro(26)] | | -------------------- | | 28: implies(or(not(p), not(q)), not(and(p, q))) [or-elim(19, 20-23, 24-27)] | -------------------- | 29: implies(or(not(p), not(q)), not(and(p, q))) [or-elim(1, 2-17, 18-28)] Proof for tautology: implies(not(or(p, q)), and(not(p), not(q))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(p, q) [or-intro(2)] | | | 6: not(not(or(p, q))) [not-not-intro(5)] | | | -------------------- | | | | 7: not(or(p, q)) [assumption(implies-intro)] | | | | 8: bottom [not-elim(6, 7)] | | | | 9: and(not(p), not(q)) [bottom(8)] | | | -------------------- | | | 10: implies(not(or(p, q)), and(not(p), not(q))) [implies-intro(7-9)] | | -------------------- | | -------------------- | | | 11: not(q) [assumption(or-elim)] | | | 12: or(p, q) [or-intro(2)] | | | 13: not(not(or(p, q))) [not-not-intro(12)] | | | -------------------- | | | | 14: not(or(p, q)) [assumption(implies-intro)] | | | | 15: bottom [not-elim(13, 14)] | | | | 16: and(not(p), not(q)) [bottom(15)] | | | -------------------- | | | 17: implies(not(or(p, q)), and(not(p), not(q))) [implies-intro(14-16)] | | -------------------- | | 18: implies(not(or(p, q)), and(not(p), not(q))) [or-elim(3, 4-10, 11-17)] | -------------------- | -------------------- | | 19: not(p) [assumption(or-elim)] | | 20: or(q, not(q)) [lem] | | -------------------- | | | 21: q [assumption(or-elim)] | | | 22: or(p, q) [or-intro(21)] | | | 23: not(not(or(p, q))) [not-not-intro(22)] | | | -------------------- | | | | 24: not(or(p, q)) [assumption(implies-intro)] | | | | 25: bottom [not-elim(23, 24)] | | | | 26: and(not(p), not(q)) [bottom(25)] | | | -------------------- | | | 27: implies(not(or(p, q)), and(not(p), not(q))) [implies-intro(24-26)] | | -------------------- | | -------------------- | | | 28: not(q) [assumption(or-elim)] | | | 29: and(not(p), not(q)) [and-intro(19, 28)] | | | 30: implies(not(or(p, q)), and(not(p), not(q))) [implies-intro(29)] | | -------------------- | | 31: implies(not(or(p, q)), and(not(p), not(q))) [or-elim(20, 21-27, 28-30)] | -------------------- | 32: implies(not(or(p, q)), and(not(p), not(q))) [or-elim(1, 2-18, 19-31)] Proof for tautology: implies(and(not(p), not(q)), not(or(p, q))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: not(not(p)) [not-not-intro(2)] | | | 6: or(not(not(p)), not(not(q))) [or-intro(5)] | | | 7: not(and(not(p), not(q))) [deMorgan(6)] | | | -------------------- | | | | 8: and(not(p), not(q)) [assumption(implies-intro)] | | | | 9: bottom [not-elim(7, 8)] | | | | 10: not(or(p, q)) [bottom(9)] | | | -------------------- | | | 11: implies(and(not(p), not(q)), not(or(p, q))) [implies-intro(8-10)] | | -------------------- | | -------------------- | | | 12: not(q) [assumption(or-elim)] | | | 13: not(not(p)) [not-not-intro(2)] | | | 14: or(not(not(p)), not(not(q))) [or-intro(13)] | | | 15: not(and(not(p), not(q))) [deMorgan(14)] | | | -------------------- | | | | 16: and(not(p), not(q)) [assumption(implies-intro)] | | | | 17: bottom [not-elim(15, 16)] | | | | 18: not(or(p, q)) [bottom(17)] | | | -------------------- | | | 19: implies(and(not(p), not(q)), not(or(p, q))) [implies-intro(16-18)] | | -------------------- | | 20: implies(and(not(p), not(q)), not(or(p, q))) [or-elim(3, 4-11, 12-19)] | -------------------- | -------------------- | | 21: not(p) [assumption(or-elim)] | | 22: or(q, not(q)) [lem] | | -------------------- | | | 23: q [assumption(or-elim)] | | | 24: not(not(q)) [not-not-intro(23)] | | | 25: or(not(not(p)), not(not(q))) [or-intro(24)] | | | 26: not(and(not(p), not(q))) [deMorgan(25)] | | | -------------------- | | | | 27: and(not(p), not(q)) [assumption(implies-intro)] | | | | 28: bottom [not-elim(26, 27)] | | | | 29: not(or(p, q)) [bottom(28)] | | | -------------------- | | | 30: implies(and(not(p), not(q)), not(or(p, q))) [implies-intro(27-29)] | | -------------------- | | -------------------- | | | 31: not(q) [assumption(or-elim)] | | | 32: and(not(p), not(q)) [and-intro(21, 31)] | | | 33: not(or(p, q)) [deMorgan(32)] | | | 34: implies(and(not(p), not(q)), not(or(p, q))) [implies-intro(33)] | | -------------------- | | 35: implies(and(not(p), not(q)), not(or(p, q))) [or-elim(22, 23-30, 31-34)] | -------------------- | 36: implies(and(not(p), not(q)), not(or(p, q))) [or-elim(1, 2-20, 21-35)] Proof for tautology: implies(and(p, or(q, r)), or(and(p, q), and(p, r))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: and(p, q) [and-intro(2, 4)] | | | | 8: or(and(p, q), and(p, r)) [or-intro(7)] | | | | 9: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(8)] | | | -------------------- | | | -------------------- | | | | 10: not(r) [assumption(or-elim)] | | | | 11: and(p, q) [and-intro(2, 4)] | | | | 12: or(and(p, q), and(p, r)) [or-intro(11)] | | | | 13: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(12)] | | | -------------------- | | | 14: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [or-elim(5, 6-9, 10-13)] | | -------------------- | | -------------------- | | | 15: not(q) [assumption(or-elim)] | | | 16: or(r, not(r)) [lem] | | | -------------------- | | | | 17: r [assumption(or-elim)] | | | | 18: and(p, r) [and-intro(2, 17)] | | | | 19: or(and(p, q), and(p, r)) [or-intro(18)] | | | | 20: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(19)] | | | -------------------- | | | -------------------- | | | | 21: not(r) [assumption(or-elim)] | | | | 22: and(not(q), not(r)) [and-intro(15, 21)] | | | | 23: not(or(q, r)) [deMorgan(22)] | | | | 24: or(not(p), not(or(q, r))) [or-intro(23)] | | | | 25: not(and(p, or(q, r))) [deMorgan(24)] | | | | -------------------- | | | | | 26: and(p, or(q, r)) [assumption(implies-intro)] | | | | | 27: bottom [not-elim(25, 26)] | | | | | 28: or(and(p, q), and(p, r)) [bottom(27)] | | | | -------------------- | | | | 29: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(26-28)] | | | -------------------- | | | 30: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [or-elim(16, 17-20, 21-29)] | | -------------------- | | 31: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [or-elim(3, 4-14, 15-30)] | -------------------- | -------------------- | | 32: not(p) [assumption(or-elim)] | | 33: or(q, not(q)) [lem] | | -------------------- | | | 34: q [assumption(or-elim)] | | | 35: or(r, not(r)) [lem] | | | -------------------- | | | | 36: r [assumption(or-elim)] | | | | 37: or(not(p), not(or(q, r))) [or-intro(32)] | | | | 38: not(and(p, or(q, r))) [deMorgan(37)] | | | | -------------------- | | | | | 39: and(p, or(q, r)) [assumption(implies-intro)] | | | | | 40: bottom [not-elim(38, 39)] | | | | | 41: or(and(p, q), and(p, r)) [bottom(40)] | | | | -------------------- | | | | 42: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(39-41)] | | | -------------------- | | | -------------------- | | | | 43: not(r) [assumption(or-elim)] | | | | 44: or(not(p), not(or(q, r))) [or-intro(32)] | | | | 45: not(and(p, or(q, r))) [deMorgan(44)] | | | | -------------------- | | | | | 46: and(p, or(q, r)) [assumption(implies-intro)] | | | | | 47: bottom [not-elim(45, 46)] | | | | | 48: or(and(p, q), and(p, r)) [bottom(47)] | | | | -------------------- | | | | 49: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(46-48)] | | | -------------------- | | | 50: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [or-elim(35, 36-42, 43-49)] | | -------------------- | | -------------------- | | | 51: not(q) [assumption(or-elim)] | | | 52: or(r, not(r)) [lem] | | | -------------------- | | | | 53: r [assumption(or-elim)] | | | | 54: or(not(p), not(or(q, r))) [or-intro(32)] | | | | 55: not(and(p, or(q, r))) [deMorgan(54)] | | | | -------------------- | | | | | 56: and(p, or(q, r)) [assumption(implies-intro)] | | | | | 57: bottom [not-elim(55, 56)] | | | | | 58: or(and(p, q), and(p, r)) [bottom(57)] | | | | -------------------- | | | | 59: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(56-58)] | | | -------------------- | | | -------------------- | | | | 60: not(r) [assumption(or-elim)] | | | | 61: or(not(p), not(or(q, r))) [or-intro(32)] | | | | 62: not(and(p, or(q, r))) [deMorgan(61)] | | | | -------------------- | | | | | 63: and(p, or(q, r)) [assumption(implies-intro)] | | | | | 64: bottom [not-elim(62, 63)] | | | | | 65: or(and(p, q), and(p, r)) [bottom(64)] | | | | -------------------- | | | | 66: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [implies-intro(63-65)] | | | -------------------- | | | 67: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [or-elim(52, 53-59, 60-66)] | | -------------------- | | 68: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [or-elim(33, 34-50, 51-67)] | -------------------- | 69: implies(and(p, or(q, r)), or(and(p, q), and(p, r))) [or-elim(1, 2-31, 32-68)] Proof for tautology: implies(or(and(p, q), and(p, r)), and(p, or(q, r))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: or(q, r) [or-intro(4)] | | | | 8: and(p, or(q, r)) [and-intro(2, 7)] | | | | 9: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(8)] | | | -------------------- | | | -------------------- | | | | 10: not(r) [assumption(or-elim)] | | | | 11: or(q, r) [or-intro(4)] | | | | 12: and(p, or(q, r)) [and-intro(2, 11)] | | | | 13: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(12)] | | | -------------------- | | | 14: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [or-elim(5, 6-9, 10-13)] | | -------------------- | | -------------------- | | | 15: not(q) [assumption(or-elim)] | | | 16: or(r, not(r)) [lem] | | | -------------------- | | | | 17: r [assumption(or-elim)] | | | | 18: or(q, r) [or-intro(17)] | | | | 19: and(p, or(q, r)) [and-intro(2, 18)] | | | | 20: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(19)] | | | -------------------- | | | -------------------- | | | | 21: not(r) [assumption(or-elim)] | | | | 22: or(not(p), not(q)) [or-intro(15)] | | | | 23: not(and(p, q)) [deMorgan(22)] | | | | 24: or(not(p), not(r)) [or-intro(21)] | | | | 25: not(and(p, r)) [deMorgan(24)] | | | | 26: and(not(and(p, q)), not(and(p, r))) [and-intro(23, 25)] | | | | 27: not(or(and(p, q), and(p, r))) [deMorgan(26)] | | | | -------------------- | | | | | 28: or(and(p, q), and(p, r)) [assumption(implies-intro)] | | | | | 29: bottom [not-elim(27, 28)] | | | | | 30: and(p, or(q, r)) [bottom(29)] | | | | -------------------- | | | | 31: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(28-30)] | | | -------------------- | | | 32: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [or-elim(16, 17-20, 21-31)] | | -------------------- | | 33: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [or-elim(3, 4-14, 15-32)] | -------------------- | -------------------- | | 34: not(p) [assumption(or-elim)] | | 35: or(q, not(q)) [lem] | | -------------------- | | | 36: q [assumption(or-elim)] | | | 37: or(r, not(r)) [lem] | | | -------------------- | | | | 38: r [assumption(or-elim)] | | | | 39: or(not(p), not(q)) [or-intro(34)] | | | | 40: not(and(p, q)) [deMorgan(39)] | | | | 41: or(not(p), not(r)) [or-intro(34)] | | | | 42: not(and(p, r)) [deMorgan(41)] | | | | 43: and(not(and(p, q)), not(and(p, r))) [and-intro(40, 42)] | | | | 44: not(or(and(p, q), and(p, r))) [deMorgan(43)] | | | | -------------------- | | | | | 45: or(and(p, q), and(p, r)) [assumption(implies-intro)] | | | | | 46: bottom [not-elim(44, 45)] | | | | | 47: and(p, or(q, r)) [bottom(46)] | | | | -------------------- | | | | 48: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(45-47)] | | | -------------------- | | | -------------------- | | | | 49: not(r) [assumption(or-elim)] | | | | 50: or(not(p), not(q)) [or-intro(34)] | | | | 51: not(and(p, q)) [deMorgan(50)] | | | | 52: or(not(p), not(r)) [or-intro(34)] | | | | 53: not(and(p, r)) [deMorgan(52)] | | | | 54: and(not(and(p, q)), not(and(p, r))) [and-intro(51, 53)] | | | | 55: not(or(and(p, q), and(p, r))) [deMorgan(54)] | | | | -------------------- | | | | | 56: or(and(p, q), and(p, r)) [assumption(implies-intro)] | | | | | 57: bottom [not-elim(55, 56)] | | | | | 58: and(p, or(q, r)) [bottom(57)] | | | | -------------------- | | | | 59: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(56-58)] | | | -------------------- | | | 60: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [or-elim(37, 38-48, 49-59)] | | -------------------- | | -------------------- | | | 61: not(q) [assumption(or-elim)] | | | 62: or(r, not(r)) [lem] | | | -------------------- | | | | 63: r [assumption(or-elim)] | | | | 64: or(not(p), not(q)) [or-intro(34)] | | | | 65: not(and(p, q)) [deMorgan(64)] | | | | 66: or(not(p), not(r)) [or-intro(34)] | | | | 67: not(and(p, r)) [deMorgan(66)] | | | | 68: and(not(and(p, q)), not(and(p, r))) [and-intro(65, 67)] | | | | 69: not(or(and(p, q), and(p, r))) [deMorgan(68)] | | | | -------------------- | | | | | 70: or(and(p, q), and(p, r)) [assumption(implies-intro)] | | | | | 71: bottom [not-elim(69, 70)] | | | | | 72: and(p, or(q, r)) [bottom(71)] | | | | -------------------- | | | | 73: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(70-72)] | | | -------------------- | | | -------------------- | | | | 74: not(r) [assumption(or-elim)] | | | | 75: or(not(p), not(q)) [or-intro(34)] | | | | 76: not(and(p, q)) [deMorgan(75)] | | | | 77: or(not(p), not(r)) [or-intro(34)] | | | | 78: not(and(p, r)) [deMorgan(77)] | | | | 79: and(not(and(p, q)), not(and(p, r))) [and-intro(76, 78)] | | | | 80: not(or(and(p, q), and(p, r))) [deMorgan(79)] | | | | -------------------- | | | | | 81: or(and(p, q), and(p, r)) [assumption(implies-intro)] | | | | | 82: bottom [not-elim(80, 81)] | | | | | 83: and(p, or(q, r)) [bottom(82)] | | | | -------------------- | | | | 84: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [implies-intro(81-83)] | | | -------------------- | | | 85: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [or-elim(62, 63-73, 74-84)] | | -------------------- | | 86: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [or-elim(35, 36-60, 61-85)] | -------------------- | 87: implies(or(and(p, q), and(p, r)), and(p, or(q, r))) [or-elim(1, 2-33, 34-86)] Proof for tautology: implies(and(or(q, r), p), or(and(q, p), and(r, p))): | 1: or(q, not(q)) [lem] | -------------------- | | 2: q [assumption(or-elim)] | | 3: or(r, not(r)) [lem] | | -------------------- | | | 4: r [assumption(or-elim)] | | | 5: or(p, not(p)) [lem] | | | -------------------- | | | | 6: p [assumption(or-elim)] | | | | 7: and(q, p) [and-intro(2, 6)] | | | | 8: or(and(q, p), and(r, p)) [or-intro(7)] | | | | 9: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(8)] | | | -------------------- | | | -------------------- | | | | 10: not(p) [assumption(or-elim)] | | | | 11: or(not(or(q, r)), not(p)) [or-intro(10)] | | | | 12: not(and(or(q, r), p)) [deMorgan(11)] | | | | -------------------- | | | | | 13: and(or(q, r), p) [assumption(implies-intro)] | | | | | 14: bottom [not-elim(12, 13)] | | | | | 15: or(and(q, p), and(r, p)) [bottom(14)] | | | | -------------------- | | | | 16: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(13-15)] | | | -------------------- | | | 17: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [or-elim(5, 6-9, 10-16)] | | -------------------- | | -------------------- | | | 18: not(r) [assumption(or-elim)] | | | 19: or(p, not(p)) [lem] | | | -------------------- | | | | 20: p [assumption(or-elim)] | | | | 21: and(q, p) [and-intro(2, 20)] | | | | 22: or(and(q, p), and(r, p)) [or-intro(21)] | | | | 23: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(22)] | | | -------------------- | | | -------------------- | | | | 24: not(p) [assumption(or-elim)] | | | | 25: or(not(or(q, r)), not(p)) [or-intro(24)] | | | | 26: not(and(or(q, r), p)) [deMorgan(25)] | | | | -------------------- | | | | | 27: and(or(q, r), p) [assumption(implies-intro)] | | | | | 28: bottom [not-elim(26, 27)] | | | | | 29: or(and(q, p), and(r, p)) [bottom(28)] | | | | -------------------- | | | | 30: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(27-29)] | | | -------------------- | | | 31: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [or-elim(19, 20-23, 24-30)] | | -------------------- | | 32: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [or-elim(3, 4-17, 18-31)] | -------------------- | -------------------- | | 33: not(q) [assumption(or-elim)] | | 34: or(r, not(r)) [lem] | | -------------------- | | | 35: r [assumption(or-elim)] | | | 36: or(p, not(p)) [lem] | | | -------------------- | | | | 37: p [assumption(or-elim)] | | | | 38: and(r, p) [and-intro(35, 37)] | | | | 39: or(and(q, p), and(r, p)) [or-intro(38)] | | | | 40: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(39)] | | | -------------------- | | | -------------------- | | | | 41: not(p) [assumption(or-elim)] | | | | 42: or(not(or(q, r)), not(p)) [or-intro(41)] | | | | 43: not(and(or(q, r), p)) [deMorgan(42)] | | | | -------------------- | | | | | 44: and(or(q, r), p) [assumption(implies-intro)] | | | | | 45: bottom [not-elim(43, 44)] | | | | | 46: or(and(q, p), and(r, p)) [bottom(45)] | | | | -------------------- | | | | 47: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(44-46)] | | | -------------------- | | | 48: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [or-elim(36, 37-40, 41-47)] | | -------------------- | | -------------------- | | | 49: not(r) [assumption(or-elim)] | | | 50: or(p, not(p)) [lem] | | | -------------------- | | | | 51: p [assumption(or-elim)] | | | | 52: and(not(q), not(r)) [and-intro(33, 49)] | | | | 53: not(or(q, r)) [deMorgan(52)] | | | | 54: or(not(or(q, r)), not(p)) [or-intro(53)] | | | | 55: not(and(or(q, r), p)) [deMorgan(54)] | | | | -------------------- | | | | | 56: and(or(q, r), p) [assumption(implies-intro)] | | | | | 57: bottom [not-elim(55, 56)] | | | | | 58: or(and(q, p), and(r, p)) [bottom(57)] | | | | -------------------- | | | | 59: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(56-58)] | | | -------------------- | | | -------------------- | | | | 60: not(p) [assumption(or-elim)] | | | | 61: and(not(q), not(r)) [and-intro(33, 49)] | | | | 62: not(or(q, r)) [deMorgan(61)] | | | | 63: or(not(or(q, r)), not(p)) [or-intro(62)] | | | | 64: not(and(or(q, r), p)) [deMorgan(63)] | | | | -------------------- | | | | | 65: and(or(q, r), p) [assumption(implies-intro)] | | | | | 66: bottom [not-elim(64, 65)] | | | | | 67: or(and(q, p), and(r, p)) [bottom(66)] | | | | -------------------- | | | | 68: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [implies-intro(65-67)] | | | -------------------- | | | 69: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [or-elim(50, 51-59, 60-68)] | | -------------------- | | 70: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [or-elim(34, 35-48, 49-69)] | -------------------- | 71: implies(and(or(q, r), p), or(and(q, p), and(r, p))) [or-elim(1, 2-32, 33-70)] Proof for tautology: implies(or(and(q, p), and(r, p)), and(or(q, r), p)): | 1: or(q, not(q)) [lem] | -------------------- | | 2: q [assumption(or-elim)] | | 3: or(p, not(p)) [lem] | | -------------------- | | | 4: p [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: or(q, r) [or-intro(2)] | | | | 8: and(or(q, r), p) [and-intro(7, 4)] | | | | 9: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(8)] | | | -------------------- | | | -------------------- | | | | 10: not(r) [assumption(or-elim)] | | | | 11: or(q, r) [or-intro(2)] | | | | 12: and(or(q, r), p) [and-intro(11, 4)] | | | | 13: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(12)] | | | -------------------- | | | 14: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [or-elim(5, 6-9, 10-13)] | | -------------------- | | -------------------- | | | 15: not(p) [assumption(or-elim)] | | | 16: or(r, not(r)) [lem] | | | -------------------- | | | | 17: r [assumption(or-elim)] | | | | 18: or(not(q), not(p)) [or-intro(15)] | | | | 19: not(and(q, p)) [deMorgan(18)] | | | | 20: or(not(r), not(p)) [or-intro(15)] | | | | 21: not(and(r, p)) [deMorgan(20)] | | | | 22: and(not(and(q, p)), not(and(r, p))) [and-intro(19, 21)] | | | | 23: not(or(and(q, p), and(r, p))) [deMorgan(22)] | | | | -------------------- | | | | | 24: or(and(q, p), and(r, p)) [assumption(implies-intro)] | | | | | 25: bottom [not-elim(23, 24)] | | | | | 26: and(or(q, r), p) [bottom(25)] | | | | -------------------- | | | | 27: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(24-26)] | | | -------------------- | | | -------------------- | | | | 28: not(r) [assumption(or-elim)] | | | | 29: or(not(q), not(p)) [or-intro(15)] | | | | 30: not(and(q, p)) [deMorgan(29)] | | | | 31: or(not(r), not(p)) [or-intro(28)] | | | | 32: not(and(r, p)) [deMorgan(31)] | | | | 33: and(not(and(q, p)), not(and(r, p))) [and-intro(30, 32)] | | | | 34: not(or(and(q, p), and(r, p))) [deMorgan(33)] | | | | -------------------- | | | | | 35: or(and(q, p), and(r, p)) [assumption(implies-intro)] | | | | | 36: bottom [not-elim(34, 35)] | | | | | 37: and(or(q, r), p) [bottom(36)] | | | | -------------------- | | | | 38: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(35-37)] | | | -------------------- | | | 39: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [or-elim(16, 17-27, 28-38)] | | -------------------- | | 40: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [or-elim(3, 4-14, 15-39)] | -------------------- | -------------------- | | 41: not(q) [assumption(or-elim)] | | 42: or(p, not(p)) [lem] | | -------------------- | | | 43: p [assumption(or-elim)] | | | 44: or(r, not(r)) [lem] | | | -------------------- | | | | 45: r [assumption(or-elim)] | | | | 46: or(q, r) [or-intro(45)] | | | | 47: and(or(q, r), p) [and-intro(46, 43)] | | | | 48: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(47)] | | | -------------------- | | | -------------------- | | | | 49: not(r) [assumption(or-elim)] | | | | 50: or(not(q), not(p)) [or-intro(41)] | | | | 51: not(and(q, p)) [deMorgan(50)] | | | | 52: or(not(r), not(p)) [or-intro(49)] | | | | 53: not(and(r, p)) [deMorgan(52)] | | | | 54: and(not(and(q, p)), not(and(r, p))) [and-intro(51, 53)] | | | | 55: not(or(and(q, p), and(r, p))) [deMorgan(54)] | | | | -------------------- | | | | | 56: or(and(q, p), and(r, p)) [assumption(implies-intro)] | | | | | 57: bottom [not-elim(55, 56)] | | | | | 58: and(or(q, r), p) [bottom(57)] | | | | -------------------- | | | | 59: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(56-58)] | | | -------------------- | | | 60: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [or-elim(44, 45-48, 49-59)] | | -------------------- | | -------------------- | | | 61: not(p) [assumption(or-elim)] | | | 62: or(r, not(r)) [lem] | | | -------------------- | | | | 63: r [assumption(or-elim)] | | | | 64: or(not(q), not(p)) [or-intro(41)] | | | | 65: not(and(q, p)) [deMorgan(64)] | | | | 66: or(not(r), not(p)) [or-intro(61)] | | | | 67: not(and(r, p)) [deMorgan(66)] | | | | 68: and(not(and(q, p)), not(and(r, p))) [and-intro(65, 67)] | | | | 69: not(or(and(q, p), and(r, p))) [deMorgan(68)] | | | | -------------------- | | | | | 70: or(and(q, p), and(r, p)) [assumption(implies-intro)] | | | | | 71: bottom [not-elim(69, 70)] | | | | | 72: and(or(q, r), p) [bottom(71)] | | | | -------------------- | | | | 73: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(70-72)] | | | -------------------- | | | -------------------- | | | | 74: not(r) [assumption(or-elim)] | | | | 75: or(not(q), not(p)) [or-intro(41)] | | | | 76: not(and(q, p)) [deMorgan(75)] | | | | 77: or(not(r), not(p)) [or-intro(74)] | | | | 78: not(and(r, p)) [deMorgan(77)] | | | | 79: and(not(and(q, p)), not(and(r, p))) [and-intro(76, 78)] | | | | 80: not(or(and(q, p), and(r, p))) [deMorgan(79)] | | | | -------------------- | | | | | 81: or(and(q, p), and(r, p)) [assumption(implies-intro)] | | | | | 82: bottom [not-elim(80, 81)] | | | | | 83: and(or(q, r), p) [bottom(82)] | | | | -------------------- | | | | 84: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [implies-intro(81-83)] | | | -------------------- | | | 85: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [or-elim(62, 63-73, 74-84)] | | -------------------- | | 86: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [or-elim(42, 43-60, 61-85)] | -------------------- | 87: implies(or(and(q, p), and(r, p)), and(or(q, r), p)) [or-elim(1, 2-40, 41-86)] Proof for tautology: implies(or(p, and(q, r)), and(or(p, q), or(p, r))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: or(p, r) [or-intro(2)] | | | | 8: or(p, q) [or-intro(2)] | | | | 9: and(or(p, q), or(p, r)) [and-intro(8, 7)] | | | | 10: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(9)] | | | -------------------- | | | -------------------- | | | | 11: not(r) [assumption(or-elim)] | | | | 12: or(p, r) [or-intro(2)] | | | | 13: or(p, q) [or-intro(2)] | | | | 14: and(or(p, q), or(p, r)) [and-intro(13, 12)] | | | | 15: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(14)] | | | -------------------- | | | 16: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [or-elim(5, 6-10, 11-15)] | | -------------------- | | -------------------- | | | 17: not(q) [assumption(or-elim)] | | | 18: or(r, not(r)) [lem] | | | -------------------- | | | | 19: r [assumption(or-elim)] | | | | 20: or(p, r) [or-intro(2)] | | | | 21: or(p, q) [or-intro(2)] | | | | 22: and(or(p, q), or(p, r)) [and-intro(21, 20)] | | | | 23: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(22)] | | | -------------------- | | | -------------------- | | | | 24: not(r) [assumption(or-elim)] | | | | 25: or(p, r) [or-intro(2)] | | | | 26: or(p, q) [or-intro(2)] | | | | 27: and(or(p, q), or(p, r)) [and-intro(26, 25)] | | | | 28: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(27)] | | | -------------------- | | | 29: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [or-elim(18, 19-23, 24-28)] | | -------------------- | | 30: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [or-elim(3, 4-16, 17-29)] | -------------------- | -------------------- | | 31: not(p) [assumption(or-elim)] | | 32: or(q, not(q)) [lem] | | -------------------- | | | 33: q [assumption(or-elim)] | | | 34: or(r, not(r)) [lem] | | | -------------------- | | | | 35: r [assumption(or-elim)] | | | | 36: or(p, r) [or-intro(35)] | | | | 37: or(p, q) [or-intro(33)] | | | | 38: and(or(p, q), or(p, r)) [and-intro(37, 36)] | | | | 39: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(38)] | | | -------------------- | | | -------------------- | | | | 40: not(r) [assumption(or-elim)] | | | | 41: or(not(q), not(r)) [or-intro(40)] | | | | 42: not(and(q, r)) [deMorgan(41)] | | | | 43: and(not(p), not(and(q, r))) [and-intro(31, 42)] | | | | 44: not(or(p, and(q, r))) [deMorgan(43)] | | | | -------------------- | | | | | 45: or(p, and(q, r)) [assumption(implies-intro)] | | | | | 46: bottom [not-elim(44, 45)] | | | | | 47: and(or(p, q), or(p, r)) [bottom(46)] | | | | -------------------- | | | | 48: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(45-47)] | | | -------------------- | | | 49: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [or-elim(34, 35-39, 40-48)] | | -------------------- | | -------------------- | | | 50: not(q) [assumption(or-elim)] | | | 51: or(r, not(r)) [lem] | | | -------------------- | | | | 52: r [assumption(or-elim)] | | | | 53: or(not(q), not(r)) [or-intro(50)] | | | | 54: not(and(q, r)) [deMorgan(53)] | | | | 55: and(not(p), not(and(q, r))) [and-intro(31, 54)] | | | | 56: not(or(p, and(q, r))) [deMorgan(55)] | | | | -------------------- | | | | | 57: or(p, and(q, r)) [assumption(implies-intro)] | | | | | 58: bottom [not-elim(56, 57)] | | | | | 59: and(or(p, q), or(p, r)) [bottom(58)] | | | | -------------------- | | | | 60: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(57-59)] | | | -------------------- | | | -------------------- | | | | 61: not(r) [assumption(or-elim)] | | | | 62: or(not(q), not(r)) [or-intro(50)] | | | | 63: not(and(q, r)) [deMorgan(62)] | | | | 64: and(not(p), not(and(q, r))) [and-intro(31, 63)] | | | | 65: not(or(p, and(q, r))) [deMorgan(64)] | | | | -------------------- | | | | | 66: or(p, and(q, r)) [assumption(implies-intro)] | | | | | 67: bottom [not-elim(65, 66)] | | | | | 68: and(or(p, q), or(p, r)) [bottom(67)] | | | | -------------------- | | | | 69: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [implies-intro(66-68)] | | | -------------------- | | | 70: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [or-elim(51, 52-60, 61-69)] | | -------------------- | | 71: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [or-elim(32, 33-49, 50-70)] | -------------------- | 72: implies(or(p, and(q, r)), and(or(p, q), or(p, r))) [or-elim(1, 2-30, 31-71)] Proof for tautology: implies(and(or(p, q), or(p, r)), or(p, and(q, r))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: or(p, and(q, r)) [or-intro(2)] | | | | 8: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(7)] | | | -------------------- | | | -------------------- | | | | 9: not(r) [assumption(or-elim)] | | | | 10: or(p, and(q, r)) [or-intro(2)] | | | | 11: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(10)] | | | -------------------- | | | 12: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [or-elim(5, 6-8, 9-11)] | | -------------------- | | -------------------- | | | 13: not(q) [assumption(or-elim)] | | | 14: or(r, not(r)) [lem] | | | -------------------- | | | | 15: r [assumption(or-elim)] | | | | 16: or(p, and(q, r)) [or-intro(2)] | | | | 17: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(16)] | | | -------------------- | | | -------------------- | | | | 18: not(r) [assumption(or-elim)] | | | | 19: or(p, and(q, r)) [or-intro(2)] | | | | 20: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(19)] | | | -------------------- | | | 21: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [or-elim(14, 15-17, 18-20)] | | -------------------- | | 22: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [or-elim(3, 4-12, 13-21)] | -------------------- | -------------------- | | 23: not(p) [assumption(or-elim)] | | 24: or(q, not(q)) [lem] | | -------------------- | | | 25: q [assumption(or-elim)] | | | 26: or(r, not(r)) [lem] | | | -------------------- | | | | 27: r [assumption(or-elim)] | | | | 28: and(q, r) [and-intro(25, 27)] | | | | 29: or(p, and(q, r)) [or-intro(28)] | | | | 30: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(29)] | | | -------------------- | | | -------------------- | | | | 31: not(r) [assumption(or-elim)] | | | | 32: and(not(p), not(r)) [and-intro(23, 31)] | | | | 33: not(or(p, r)) [deMorgan(32)] | | | | 34: or(not(or(p, q)), not(or(p, r))) [or-intro(33)] | | | | 35: not(and(or(p, q), or(p, r))) [deMorgan(34)] | | | | -------------------- | | | | | 36: and(or(p, q), or(p, r)) [assumption(implies-intro)] | | | | | 37: bottom [not-elim(35, 36)] | | | | | 38: or(p, and(q, r)) [bottom(37)] | | | | -------------------- | | | | 39: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(36-38)] | | | -------------------- | | | 40: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [or-elim(26, 27-30, 31-39)] | | -------------------- | | -------------------- | | | 41: not(q) [assumption(or-elim)] | | | 42: or(r, not(r)) [lem] | | | -------------------- | | | | 43: r [assumption(or-elim)] | | | | 44: and(not(p), not(q)) [and-intro(23, 41)] | | | | 45: not(or(p, q)) [deMorgan(44)] | | | | 46: or(not(or(p, q)), not(or(p, r))) [or-intro(45)] | | | | 47: not(and(or(p, q), or(p, r))) [deMorgan(46)] | | | | -------------------- | | | | | 48: and(or(p, q), or(p, r)) [assumption(implies-intro)] | | | | | 49: bottom [not-elim(47, 48)] | | | | | 50: or(p, and(q, r)) [bottom(49)] | | | | -------------------- | | | | 51: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(48-50)] | | | -------------------- | | | -------------------- | | | | 52: not(r) [assumption(or-elim)] | | | | 53: and(not(p), not(q)) [and-intro(23, 41)] | | | | 54: not(or(p, q)) [deMorgan(53)] | | | | 55: or(not(or(p, q)), not(or(p, r))) [or-intro(54)] | | | | 56: not(and(or(p, q), or(p, r))) [deMorgan(55)] | | | | -------------------- | | | | | 57: and(or(p, q), or(p, r)) [assumption(implies-intro)] | | | | | 58: bottom [not-elim(56, 57)] | | | | | 59: or(p, and(q, r)) [bottom(58)] | | | | -------------------- | | | | 60: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [implies-intro(57-59)] | | | -------------------- | | | 61: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [or-elim(42, 43-51, 52-60)] | | -------------------- | | 62: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [or-elim(24, 25-40, 41-61)] | -------------------- | 63: implies(and(or(p, q), or(p, r)), or(p, and(q, r))) [or-elim(1, 2-22, 23-62)] Proof for tautology: implies(or(and(q, r), p), and(or(q, p), or(r, p))): | 1: or(q, not(q)) [lem] | -------------------- | | 2: q [assumption(or-elim)] | | 3: or(r, not(r)) [lem] | | -------------------- | | | 4: r [assumption(or-elim)] | | | 5: or(p, not(p)) [lem] | | | -------------------- | | | | 6: p [assumption(or-elim)] | | | | 7: or(r, p) [or-intro(4)] | | | | 8: or(q, p) [or-intro(2)] | | | | 9: and(or(q, p), or(r, p)) [and-intro(8, 7)] | | | | 10: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(9)] | | | -------------------- | | | -------------------- | | | | 11: not(p) [assumption(or-elim)] | | | | 12: or(r, p) [or-intro(4)] | | | | 13: or(q, p) [or-intro(2)] | | | | 14: and(or(q, p), or(r, p)) [and-intro(13, 12)] | | | | 15: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(14)] | | | -------------------- | | | 16: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [or-elim(5, 6-10, 11-15)] | | -------------------- | | -------------------- | | | 17: not(r) [assumption(or-elim)] | | | 18: or(p, not(p)) [lem] | | | -------------------- | | | | 19: p [assumption(or-elim)] | | | | 20: or(r, p) [or-intro(19)] | | | | 21: or(q, p) [or-intro(2)] | | | | 22: and(or(q, p), or(r, p)) [and-intro(21, 20)] | | | | 23: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(22)] | | | -------------------- | | | -------------------- | | | | 24: not(p) [assumption(or-elim)] | | | | 25: or(not(q), not(r)) [or-intro(17)] | | | | 26: not(and(q, r)) [deMorgan(25)] | | | | 27: and(not(and(q, r)), not(p)) [and-intro(26, 24)] | | | | 28: not(or(and(q, r), p)) [deMorgan(27)] | | | | -------------------- | | | | | 29: or(and(q, r), p) [assumption(implies-intro)] | | | | | 30: bottom [not-elim(28, 29)] | | | | | 31: and(or(q, p), or(r, p)) [bottom(30)] | | | | -------------------- | | | | 32: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(29-31)] | | | -------------------- | | | 33: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [or-elim(18, 19-23, 24-32)] | | -------------------- | | 34: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [or-elim(3, 4-16, 17-33)] | -------------------- | -------------------- | | 35: not(q) [assumption(or-elim)] | | 36: or(r, not(r)) [lem] | | -------------------- | | | 37: r [assumption(or-elim)] | | | 38: or(p, not(p)) [lem] | | | -------------------- | | | | 39: p [assumption(or-elim)] | | | | 40: or(r, p) [or-intro(37)] | | | | 41: or(q, p) [or-intro(39)] | | | | 42: and(or(q, p), or(r, p)) [and-intro(41, 40)] | | | | 43: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(42)] | | | -------------------- | | | -------------------- | | | | 44: not(p) [assumption(or-elim)] | | | | 45: or(not(q), not(r)) [or-intro(35)] | | | | 46: not(and(q, r)) [deMorgan(45)] | | | | 47: and(not(and(q, r)), not(p)) [and-intro(46, 44)] | | | | 48: not(or(and(q, r), p)) [deMorgan(47)] | | | | -------------------- | | | | | 49: or(and(q, r), p) [assumption(implies-intro)] | | | | | 50: bottom [not-elim(48, 49)] | | | | | 51: and(or(q, p), or(r, p)) [bottom(50)] | | | | -------------------- | | | | 52: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(49-51)] | | | -------------------- | | | 53: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [or-elim(38, 39-43, 44-52)] | | -------------------- | | -------------------- | | | 54: not(r) [assumption(or-elim)] | | | 55: or(p, not(p)) [lem] | | | -------------------- | | | | 56: p [assumption(or-elim)] | | | | 57: or(r, p) [or-intro(56)] | | | | 58: or(q, p) [or-intro(56)] | | | | 59: and(or(q, p), or(r, p)) [and-intro(58, 57)] | | | | 60: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(59)] | | | -------------------- | | | -------------------- | | | | 61: not(p) [assumption(or-elim)] | | | | 62: or(not(q), not(r)) [or-intro(35)] | | | | 63: not(and(q, r)) [deMorgan(62)] | | | | 64: and(not(and(q, r)), not(p)) [and-intro(63, 61)] | | | | 65: not(or(and(q, r), p)) [deMorgan(64)] | | | | -------------------- | | | | | 66: or(and(q, r), p) [assumption(implies-intro)] | | | | | 67: bottom [not-elim(65, 66)] | | | | | 68: and(or(q, p), or(r, p)) [bottom(67)] | | | | -------------------- | | | | 69: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [implies-intro(66-68)] | | | -------------------- | | | 70: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [or-elim(55, 56-60, 61-69)] | | -------------------- | | 71: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [or-elim(36, 37-53, 54-70)] | -------------------- | 72: implies(or(and(q, r), p), and(or(q, p), or(r, p))) [or-elim(1, 2-34, 35-71)] Proof for tautology: implies(and(or(q, p), or(r, p)), or(and(q, r), p)): | 1: or(q, not(q)) [lem] | -------------------- | | 2: q [assumption(or-elim)] | | 3: or(p, not(p)) [lem] | | -------------------- | | | 4: p [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: and(q, r) [and-intro(2, 6)] | | | | 8: or(and(q, r), p) [or-intro(7)] | | | | 9: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(8)] | | | -------------------- | | | -------------------- | | | | 10: not(r) [assumption(or-elim)] | | | | 11: or(and(q, r), p) [or-intro(4)] | | | | 12: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(11)] | | | -------------------- | | | 13: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [or-elim(5, 6-9, 10-12)] | | -------------------- | | -------------------- | | | 14: not(p) [assumption(or-elim)] | | | 15: or(r, not(r)) [lem] | | | -------------------- | | | | 16: r [assumption(or-elim)] | | | | 17: and(q, r) [and-intro(2, 16)] | | | | 18: or(and(q, r), p) [or-intro(17)] | | | | 19: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(18)] | | | -------------------- | | | -------------------- | | | | 20: not(r) [assumption(or-elim)] | | | | 21: and(not(r), not(p)) [and-intro(20, 14)] | | | | 22: not(or(r, p)) [deMorgan(21)] | | | | 23: or(not(or(q, p)), not(or(r, p))) [or-intro(22)] | | | | 24: not(and(or(q, p), or(r, p))) [deMorgan(23)] | | | | -------------------- | | | | | 25: and(or(q, p), or(r, p)) [assumption(implies-intro)] | | | | | 26: bottom [not-elim(24, 25)] | | | | | 27: or(and(q, r), p) [bottom(26)] | | | | -------------------- | | | | 28: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(25-27)] | | | -------------------- | | | 29: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [or-elim(15, 16-19, 20-28)] | | -------------------- | | 30: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [or-elim(3, 4-13, 14-29)] | -------------------- | -------------------- | | 31: not(q) [assumption(or-elim)] | | 32: or(p, not(p)) [lem] | | -------------------- | | | 33: p [assumption(or-elim)] | | | 34: or(r, not(r)) [lem] | | | -------------------- | | | | 35: r [assumption(or-elim)] | | | | 36: or(and(q, r), p) [or-intro(33)] | | | | 37: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(36)] | | | -------------------- | | | -------------------- | | | | 38: not(r) [assumption(or-elim)] | | | | 39: or(and(q, r), p) [or-intro(33)] | | | | 40: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(39)] | | | -------------------- | | | 41: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [or-elim(34, 35-37, 38-40)] | | -------------------- | | -------------------- | | | 42: not(p) [assumption(or-elim)] | | | 43: or(r, not(r)) [lem] | | | -------------------- | | | | 44: r [assumption(or-elim)] | | | | 45: and(not(q), not(p)) [and-intro(31, 42)] | | | | 46: not(or(q, p)) [deMorgan(45)] | | | | 47: or(not(or(q, p)), not(or(r, p))) [or-intro(46)] | | | | 48: not(and(or(q, p), or(r, p))) [deMorgan(47)] | | | | -------------------- | | | | | 49: and(or(q, p), or(r, p)) [assumption(implies-intro)] | | | | | 50: bottom [not-elim(48, 49)] | | | | | 51: or(and(q, r), p) [bottom(50)] | | | | -------------------- | | | | 52: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(49-51)] | | | -------------------- | | | -------------------- | | | | 53: not(r) [assumption(or-elim)] | | | | 54: and(not(q), not(p)) [and-intro(31, 42)] | | | | 55: not(or(q, p)) [deMorgan(54)] | | | | 56: or(not(or(q, p)), not(or(r, p))) [or-intro(55)] | | | | 57: not(and(or(q, p), or(r, p))) [deMorgan(56)] | | | | -------------------- | | | | | 58: and(or(q, p), or(r, p)) [assumption(implies-intro)] | | | | | 59: bottom [not-elim(57, 58)] | | | | | 60: or(and(q, r), p) [bottom(59)] | | | | -------------------- | | | | 61: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [implies-intro(58-60)] | | | -------------------- | | | 62: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [or-elim(43, 44-52, 53-61)] | | -------------------- | | 63: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [or-elim(32, 33-41, 42-62)] | -------------------- | 64: implies(and(or(q, p), or(r, p)), or(and(q, r), p)) [or-elim(1, 2-30, 31-63)] Proof for tautology: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: or(s, not(s)) [lem] | | | | -------------------- | | | | | 8: s [assumption(or-elim)] | | | | | 9: and(q, s) [and-intro(4, 8)] | | | | | 10: implies(and(p, r), and(q, s)) [implies-intro(9)] | | | | | 11: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(10)] | | | | -------------------- | | | | -------------------- | | | | | 12: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 13: implies(r, s) [assumption(not-intro)] | | | | | | 14: s [implies-elim(6, 13)] | | | | | | 15: bottom [not-elim(12, 14)] | | | | | -------------------- | | | | | 16: not(implies(r, s)) [not-intro(13-15)] | | | | | 17: or(not(implies(p, q)), not(implies(r, s))) [or-intro(16)] | | | | | 18: not(and(implies(p, q), implies(r, s))) [deMorgan(17)] | | | | | -------------------- | | | | | | 19: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 20: bottom [not-elim(18, 19)] | | | | | | 21: implies(and(p, r), and(q, s)) [bottom(20)] | | | | | -------------------- | | | | | 22: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(19-21)] | | | | -------------------- | | | | 23: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(7, 8-11, 12-22)] | | | -------------------- | | | -------------------- | | | | 24: not(r) [assumption(or-elim)] | | | | 25: or(s, not(s)) [lem] | | | | -------------------- | | | | | 26: s [assumption(or-elim)] | | | | | 27: or(not(p), not(r)) [or-intro(24)] | | | | | 28: not(and(p, r)) [deMorgan(27)] | | | | | -------------------- | | | | | | 29: and(p, r) [assumption(implies-intro)] | | | | | | 30: bottom [not-elim(28, 29)] | | | | | | 31: and(q, s) [bottom(30)] | | | | | -------------------- | | | | | 32: implies(and(p, r), and(q, s)) [implies-intro(29-31)] | | | | | 33: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(32)] | | | | -------------------- | | | | -------------------- | | | | | 34: not(s) [assumption(or-elim)] | | | | | 35: or(not(p), not(r)) [or-intro(24)] | | | | | 36: not(and(p, r)) [deMorgan(35)] | | | | | -------------------- | | | | | | 37: and(p, r) [assumption(implies-intro)] | | | | | | 38: bottom [not-elim(36, 37)] | | | | | | 39: and(q, s) [bottom(38)] | | | | | -------------------- | | | | | 40: implies(and(p, r), and(q, s)) [implies-intro(37-39)] | | | | | 41: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(40)] | | | | -------------------- | | | | 42: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(25, 26-33, 34-41)] | | | -------------------- | | | 43: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(5, 6-23, 24-42)] | | -------------------- | | -------------------- | | | 44: not(q) [assumption(or-elim)] | | | 45: or(r, not(r)) [lem] | | | -------------------- | | | | 46: r [assumption(or-elim)] | | | | 47: or(s, not(s)) [lem] | | | | -------------------- | | | | | 48: s [assumption(or-elim)] | | | | | -------------------- | | | | | | 49: implies(p, q) [assumption(not-intro)] | | | | | | 50: q [implies-elim(2, 49)] | | | | | | 51: bottom [not-elim(44, 50)] | | | | | -------------------- | | | | | 52: not(implies(p, q)) [not-intro(49-51)] | | | | | 53: or(not(implies(p, q)), not(implies(r, s))) [or-intro(52)] | | | | | 54: not(and(implies(p, q), implies(r, s))) [deMorgan(53)] | | | | | -------------------- | | | | | | 55: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 56: bottom [not-elim(54, 55)] | | | | | | 57: implies(and(p, r), and(q, s)) [bottom(56)] | | | | | -------------------- | | | | | 58: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(55-57)] | | | | -------------------- | | | | -------------------- | | | | | 59: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 60: implies(p, q) [assumption(not-intro)] | | | | | | 61: q [implies-elim(2, 60)] | | | | | | 62: bottom [not-elim(44, 61)] | | | | | -------------------- | | | | | 63: not(implies(p, q)) [not-intro(60-62)] | | | | | 64: or(not(implies(p, q)), not(implies(r, s))) [or-intro(63)] | | | | | 65: not(and(implies(p, q), implies(r, s))) [deMorgan(64)] | | | | | -------------------- | | | | | | 66: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 67: bottom [not-elim(65, 66)] | | | | | | 68: implies(and(p, r), and(q, s)) [bottom(67)] | | | | | -------------------- | | | | | 69: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(66-68)] | | | | -------------------- | | | | 70: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(47, 48-58, 59-69)] | | | -------------------- | | | -------------------- | | | | 71: not(r) [assumption(or-elim)] | | | | 72: or(s, not(s)) [lem] | | | | -------------------- | | | | | 73: s [assumption(or-elim)] | | | | | -------------------- | | | | | | 74: implies(p, q) [assumption(not-intro)] | | | | | | 75: q [implies-elim(2, 74)] | | | | | | 76: bottom [not-elim(44, 75)] | | | | | -------------------- | | | | | 77: not(implies(p, q)) [not-intro(74-76)] | | | | | 78: or(not(implies(p, q)), not(implies(r, s))) [or-intro(77)] | | | | | 79: not(and(implies(p, q), implies(r, s))) [deMorgan(78)] | | | | | -------------------- | | | | | | 80: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 81: bottom [not-elim(79, 80)] | | | | | | 82: implies(and(p, r), and(q, s)) [bottom(81)] | | | | | -------------------- | | | | | 83: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(80-82)] | | | | -------------------- | | | | -------------------- | | | | | 84: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 85: implies(p, q) [assumption(not-intro)] | | | | | | 86: q [implies-elim(2, 85)] | | | | | | 87: bottom [not-elim(44, 86)] | | | | | -------------------- | | | | | 88: not(implies(p, q)) [not-intro(85-87)] | | | | | 89: or(not(implies(p, q)), not(implies(r, s))) [or-intro(88)] | | | | | 90: not(and(implies(p, q), implies(r, s))) [deMorgan(89)] | | | | | -------------------- | | | | | | 91: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 92: bottom [not-elim(90, 91)] | | | | | | 93: implies(and(p, r), and(q, s)) [bottom(92)] | | | | | -------------------- | | | | | 94: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(91-93)] | | | | -------------------- | | | | 95: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(72, 73-83, 84-94)] | | | -------------------- | | | 96: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(45, 46-70, 71-95)] | | -------------------- | | 97: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(3, 4-43, 44-96)] | -------------------- | -------------------- | | 98: not(p) [assumption(or-elim)] | | 99: or(q, not(q)) [lem] | | -------------------- | | | 100: q [assumption(or-elim)] | | | 101: or(r, not(r)) [lem] | | | -------------------- | | | | 102: r [assumption(or-elim)] | | | | 103: or(s, not(s)) [lem] | | | | -------------------- | | | | | 104: s [assumption(or-elim)] | | | | | 105: or(not(p), not(r)) [or-intro(98)] | | | | | 106: not(and(p, r)) [deMorgan(105)] | | | | | -------------------- | | | | | | 107: and(p, r) [assumption(implies-intro)] | | | | | | 108: bottom [not-elim(106, 107)] | | | | | | 109: and(q, s) [bottom(108)] | | | | | -------------------- | | | | | 110: implies(and(p, r), and(q, s)) [implies-intro(107-109)] | | | | | 111: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(110)] | | | | -------------------- | | | | -------------------- | | | | | 112: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 113: implies(r, s) [assumption(not-intro)] | | | | | | 114: s [implies-elim(102, 113)] | | | | | | 115: bottom [not-elim(112, 114)] | | | | | -------------------- | | | | | 116: not(implies(r, s)) [not-intro(113-115)] | | | | | 117: or(not(implies(p, q)), not(implies(r, s))) [or-intro(116)] | | | | | 118: not(and(implies(p, q), implies(r, s))) [deMorgan(117)] | | | | | -------------------- | | | | | | 119: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 120: bottom [not-elim(118, 119)] | | | | | | 121: implies(and(p, r), and(q, s)) [bottom(120)] | | | | | -------------------- | | | | | 122: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(119-121)] | | | | -------------------- | | | | 123: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(103, 104-111, 112-122)] | | | -------------------- | | | -------------------- | | | | 124: not(r) [assumption(or-elim)] | | | | 125: or(s, not(s)) [lem] | | | | -------------------- | | | | | 126: s [assumption(or-elim)] | | | | | 127: or(not(p), not(r)) [or-intro(98)] | | | | | 128: not(and(p, r)) [deMorgan(127)] | | | | | -------------------- | | | | | | 129: and(p, r) [assumption(implies-intro)] | | | | | | 130: bottom [not-elim(128, 129)] | | | | | | 131: and(q, s) [bottom(130)] | | | | | -------------------- | | | | | 132: implies(and(p, r), and(q, s)) [implies-intro(129-131)] | | | | | 133: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(132)] | | | | -------------------- | | | | -------------------- | | | | | 134: not(s) [assumption(or-elim)] | | | | | 135: or(not(p), not(r)) [or-intro(98)] | | | | | 136: not(and(p, r)) [deMorgan(135)] | | | | | -------------------- | | | | | | 137: and(p, r) [assumption(implies-intro)] | | | | | | 138: bottom [not-elim(136, 137)] | | | | | | 139: and(q, s) [bottom(138)] | | | | | -------------------- | | | | | 140: implies(and(p, r), and(q, s)) [implies-intro(137-139)] | | | | | 141: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(140)] | | | | -------------------- | | | | 142: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(125, 126-133, 134-141)] | | | -------------------- | | | 143: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(101, 102-123, 124-142)] | | -------------------- | | -------------------- | | | 144: not(q) [assumption(or-elim)] | | | 145: or(r, not(r)) [lem] | | | -------------------- | | | | 146: r [assumption(or-elim)] | | | | 147: or(s, not(s)) [lem] | | | | -------------------- | | | | | 148: s [assumption(or-elim)] | | | | | 149: or(not(p), not(r)) [or-intro(98)] | | | | | 150: not(and(p, r)) [deMorgan(149)] | | | | | -------------------- | | | | | | 151: and(p, r) [assumption(implies-intro)] | | | | | | 152: bottom [not-elim(150, 151)] | | | | | | 153: and(q, s) [bottom(152)] | | | | | -------------------- | | | | | 154: implies(and(p, r), and(q, s)) [implies-intro(151-153)] | | | | | 155: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(154)] | | | | -------------------- | | | | -------------------- | | | | | 156: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 157: implies(r, s) [assumption(not-intro)] | | | | | | 158: s [implies-elim(146, 157)] | | | | | | 159: bottom [not-elim(156, 158)] | | | | | -------------------- | | | | | 160: not(implies(r, s)) [not-intro(157-159)] | | | | | 161: or(not(implies(p, q)), not(implies(r, s))) [or-intro(160)] | | | | | 162: not(and(implies(p, q), implies(r, s))) [deMorgan(161)] | | | | | -------------------- | | | | | | 163: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 164: bottom [not-elim(162, 163)] | | | | | | 165: implies(and(p, r), and(q, s)) [bottom(164)] | | | | | -------------------- | | | | | 166: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(163-165)] | | | | -------------------- | | | | 167: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(147, 148-155, 156-166)] | | | -------------------- | | | -------------------- | | | | 168: not(r) [assumption(or-elim)] | | | | 169: or(s, not(s)) [lem] | | | | -------------------- | | | | | 170: s [assumption(or-elim)] | | | | | 171: or(not(p), not(r)) [or-intro(98)] | | | | | 172: not(and(p, r)) [deMorgan(171)] | | | | | -------------------- | | | | | | 173: and(p, r) [assumption(implies-intro)] | | | | | | 174: bottom [not-elim(172, 173)] | | | | | | 175: and(q, s) [bottom(174)] | | | | | -------------------- | | | | | 176: implies(and(p, r), and(q, s)) [implies-intro(173-175)] | | | | | 177: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(176)] | | | | -------------------- | | | | -------------------- | | | | | 178: not(s) [assumption(or-elim)] | | | | | 179: or(not(p), not(r)) [or-intro(98)] | | | | | 180: not(and(p, r)) [deMorgan(179)] | | | | | -------------------- | | | | | | 181: and(p, r) [assumption(implies-intro)] | | | | | | 182: bottom [not-elim(180, 181)] | | | | | | 183: and(q, s) [bottom(182)] | | | | | -------------------- | | | | | 184: implies(and(p, r), and(q, s)) [implies-intro(181-183)] | | | | | 185: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [implies-intro(184)] | | | | -------------------- | | | | 186: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(169, 170-177, 178-185)] | | | -------------------- | | | 187: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(145, 146-167, 168-186)] | | -------------------- | | 188: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(99, 100-143, 144-187)] | -------------------- | 189: implies(and(implies(p, q), implies(r, s)), implies(and(p, r), and(q, s))) [or-elim(1, 2-97, 98-188)] Proof for tautology: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))): | 1: or(p, not(p)) [lem] | -------------------- | | 2: p [assumption(or-elim)] | | 3: or(q, not(q)) [lem] | | -------------------- | | | 4: q [assumption(or-elim)] | | | 5: or(r, not(r)) [lem] | | | -------------------- | | | | 6: r [assumption(or-elim)] | | | | 7: or(s, not(s)) [lem] | | | | -------------------- | | | | | 8: s [assumption(or-elim)] | | | | | 9: or(q, s) [or-intro(4)] | | | | | 10: implies(or(p, r), or(q, s)) [implies-intro(9)] | | | | | 11: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(10)] | | | | -------------------- | | | | -------------------- | | | | | 12: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 13: implies(r, s) [assumption(not-intro)] | | | | | | 14: s [implies-elim(6, 13)] | | | | | | 15: bottom [not-elim(12, 14)] | | | | | -------------------- | | | | | 16: not(implies(r, s)) [not-intro(13-15)] | | | | | 17: or(not(implies(p, q)), not(implies(r, s))) [or-intro(16)] | | | | | 18: not(and(implies(p, q), implies(r, s))) [deMorgan(17)] | | | | | -------------------- | | | | | | 19: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 20: bottom [not-elim(18, 19)] | | | | | | 21: implies(or(p, r), or(q, s)) [bottom(20)] | | | | | -------------------- | | | | | 22: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(19-21)] | | | | -------------------- | | | | 23: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(7, 8-11, 12-22)] | | | -------------------- | | | -------------------- | | | | 24: not(r) [assumption(or-elim)] | | | | 25: or(s, not(s)) [lem] | | | | -------------------- | | | | | 26: s [assumption(or-elim)] | | | | | 27: or(q, s) [or-intro(4)] | | | | | 28: implies(or(p, r), or(q, s)) [implies-intro(27)] | | | | | 29: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(28)] | | | | -------------------- | | | | -------------------- | | | | | 30: not(s) [assumption(or-elim)] | | | | | 31: or(q, s) [or-intro(4)] | | | | | 32: implies(or(p, r), or(q, s)) [implies-intro(31)] | | | | | 33: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(32)] | | | | -------------------- | | | | 34: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(25, 26-29, 30-33)] | | | -------------------- | | | 35: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(5, 6-23, 24-34)] | | -------------------- | | -------------------- | | | 36: not(q) [assumption(or-elim)] | | | 37: or(r, not(r)) [lem] | | | -------------------- | | | | 38: r [assumption(or-elim)] | | | | 39: or(s, not(s)) [lem] | | | | -------------------- | | | | | 40: s [assumption(or-elim)] | | | | | -------------------- | | | | | | 41: implies(p, q) [assumption(not-intro)] | | | | | | 42: q [implies-elim(2, 41)] | | | | | | 43: bottom [not-elim(36, 42)] | | | | | -------------------- | | | | | 44: not(implies(p, q)) [not-intro(41-43)] | | | | | 45: or(not(implies(p, q)), not(implies(r, s))) [or-intro(44)] | | | | | 46: not(and(implies(p, q), implies(r, s))) [deMorgan(45)] | | | | | -------------------- | | | | | | 47: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 48: bottom [not-elim(46, 47)] | | | | | | 49: implies(or(p, r), or(q, s)) [bottom(48)] | | | | | -------------------- | | | | | 50: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(47-49)] | | | | -------------------- | | | | -------------------- | | | | | 51: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 52: implies(p, q) [assumption(not-intro)] | | | | | | 53: q [implies-elim(2, 52)] | | | | | | 54: bottom [not-elim(36, 53)] | | | | | -------------------- | | | | | 55: not(implies(p, q)) [not-intro(52-54)] | | | | | 56: or(not(implies(p, q)), not(implies(r, s))) [or-intro(55)] | | | | | 57: not(and(implies(p, q), implies(r, s))) [deMorgan(56)] | | | | | -------------------- | | | | | | 58: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 59: bottom [not-elim(57, 58)] | | | | | | 60: implies(or(p, r), or(q, s)) [bottom(59)] | | | | | -------------------- | | | | | 61: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(58-60)] | | | | -------------------- | | | | 62: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(39, 40-50, 51-61)] | | | -------------------- | | | -------------------- | | | | 63: not(r) [assumption(or-elim)] | | | | 64: or(s, not(s)) [lem] | | | | -------------------- | | | | | 65: s [assumption(or-elim)] | | | | | -------------------- | | | | | | 66: implies(p, q) [assumption(not-intro)] | | | | | | 67: q [implies-elim(2, 66)] | | | | | | 68: bottom [not-elim(36, 67)] | | | | | -------------------- | | | | | 69: not(implies(p, q)) [not-intro(66-68)] | | | | | 70: or(not(implies(p, q)), not(implies(r, s))) [or-intro(69)] | | | | | 71: not(and(implies(p, q), implies(r, s))) [deMorgan(70)] | | | | | -------------------- | | | | | | 72: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 73: bottom [not-elim(71, 72)] | | | | | | 74: implies(or(p, r), or(q, s)) [bottom(73)] | | | | | -------------------- | | | | | 75: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(72-74)] | | | | -------------------- | | | | -------------------- | | | | | 76: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 77: implies(p, q) [assumption(not-intro)] | | | | | | 78: q [implies-elim(2, 77)] | | | | | | 79: bottom [not-elim(36, 78)] | | | | | -------------------- | | | | | 80: not(implies(p, q)) [not-intro(77-79)] | | | | | 81: or(not(implies(p, q)), not(implies(r, s))) [or-intro(80)] | | | | | 82: not(and(implies(p, q), implies(r, s))) [deMorgan(81)] | | | | | -------------------- | | | | | | 83: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 84: bottom [not-elim(82, 83)] | | | | | | 85: implies(or(p, r), or(q, s)) [bottom(84)] | | | | | -------------------- | | | | | 86: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(83-85)] | | | | -------------------- | | | | 87: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(64, 65-75, 76-86)] | | | -------------------- | | | 88: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(37, 38-62, 63-87)] | | -------------------- | | 89: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(3, 4-35, 36-88)] | -------------------- | -------------------- | | 90: not(p) [assumption(or-elim)] | | 91: or(q, not(q)) [lem] | | -------------------- | | | 92: q [assumption(or-elim)] | | | 93: or(r, not(r)) [lem] | | | -------------------- | | | | 94: r [assumption(or-elim)] | | | | 95: or(s, not(s)) [lem] | | | | -------------------- | | | | | 96: s [assumption(or-elim)] | | | | | 97: or(q, s) [or-intro(92)] | | | | | 98: implies(or(p, r), or(q, s)) [implies-intro(97)] | | | | | 99: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(98)] | | | | -------------------- | | | | -------------------- | | | | | 100: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 101: implies(r, s) [assumption(not-intro)] | | | | | | 102: s [implies-elim(94, 101)] | | | | | | 103: bottom [not-elim(100, 102)] | | | | | -------------------- | | | | | 104: not(implies(r, s)) [not-intro(101-103)] | | | | | 105: or(not(implies(p, q)), not(implies(r, s))) [or-intro(104)] | | | | | 106: not(and(implies(p, q), implies(r, s))) [deMorgan(105)] | | | | | -------------------- | | | | | | 107: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 108: bottom [not-elim(106, 107)] | | | | | | 109: implies(or(p, r), or(q, s)) [bottom(108)] | | | | | -------------------- | | | | | 110: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(107-109)] | | | | -------------------- | | | | 111: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(95, 96-99, 100-110)] | | | -------------------- | | | -------------------- | | | | 112: not(r) [assumption(or-elim)] | | | | 113: or(s, not(s)) [lem] | | | | -------------------- | | | | | 114: s [assumption(or-elim)] | | | | | 115: and(not(p), not(r)) [and-intro(90, 112)] | | | | | 116: not(or(p, r)) [deMorgan(115)] | | | | | -------------------- | | | | | | 117: or(p, r) [assumption(implies-intro)] | | | | | | 118: bottom [not-elim(116, 117)] | | | | | | 119: or(q, s) [bottom(118)] | | | | | -------------------- | | | | | 120: implies(or(p, r), or(q, s)) [implies-intro(117-119)] | | | | | 121: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(120)] | | | | -------------------- | | | | -------------------- | | | | | 122: not(s) [assumption(or-elim)] | | | | | 123: and(not(p), not(r)) [and-intro(90, 112)] | | | | | 124: not(or(p, r)) [deMorgan(123)] | | | | | -------------------- | | | | | | 125: or(p, r) [assumption(implies-intro)] | | | | | | 126: bottom [not-elim(124, 125)] | | | | | | 127: or(q, s) [bottom(126)] | | | | | -------------------- | | | | | 128: implies(or(p, r), or(q, s)) [implies-intro(125-127)] | | | | | 129: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(128)] | | | | -------------------- | | | | 130: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(113, 114-121, 122-129)] | | | -------------------- | | | 131: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(93, 94-111, 112-130)] | | -------------------- | | -------------------- | | | 132: not(q) [assumption(or-elim)] | | | 133: or(r, not(r)) [lem] | | | -------------------- | | | | 134: r [assumption(or-elim)] | | | | 135: or(s, not(s)) [lem] | | | | -------------------- | | | | | 136: s [assumption(or-elim)] | | | | | 137: or(q, s) [or-intro(136)] | | | | | 138: implies(or(p, r), or(q, s)) [implies-intro(137)] | | | | | 139: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(138)] | | | | -------------------- | | | | -------------------- | | | | | 140: not(s) [assumption(or-elim)] | | | | | -------------------- | | | | | | 141: implies(r, s) [assumption(not-intro)] | | | | | | 142: s [implies-elim(134, 141)] | | | | | | 143: bottom [not-elim(140, 142)] | | | | | -------------------- | | | | | 144: not(implies(r, s)) [not-intro(141-143)] | | | | | 145: or(not(implies(p, q)), not(implies(r, s))) [or-intro(144)] | | | | | 146: not(and(implies(p, q), implies(r, s))) [deMorgan(145)] | | | | | -------------------- | | | | | | 147: and(implies(p, q), implies(r, s)) [assumption(implies-intro)] | | | | | | 148: bottom [not-elim(146, 147)] | | | | | | 149: implies(or(p, r), or(q, s)) [bottom(148)] | | | | | -------------------- | | | | | 150: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(147-149)] | | | | -------------------- | | | | 151: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(135, 136-139, 140-150)] | | | -------------------- | | | -------------------- | | | | 152: not(r) [assumption(or-elim)] | | | | 153: or(s, not(s)) [lem] | | | | -------------------- | | | | | 154: s [assumption(or-elim)] | | | | | 155: and(not(p), not(r)) [and-intro(90, 152)] | | | | | 156: not(or(p, r)) [deMorgan(155)] | | | | | -------------------- | | | | | | 157: or(p, r) [assumption(implies-intro)] | | | | | | 158: bottom [not-elim(156, 157)] | | | | | | 159: or(q, s) [bottom(158)] | | | | | -------------------- | | | | | 160: implies(or(p, r), or(q, s)) [implies-intro(157-159)] | | | | | 161: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(160)] | | | | -------------------- | | | | -------------------- | | | | | 162: not(s) [assumption(or-elim)] | | | | | 163: and(not(p), not(r)) [and-intro(90, 152)] | | | | | 164: not(or(p, r)) [deMorgan(163)] | | | | | -------------------- | | | | | | 165: or(p, r) [assumption(implies-intro)] | | | | | | 166: bottom [not-elim(164, 165)] | | | | | | 167: or(q, s) [bottom(166)] | | | | | -------------------- | | | | | 168: implies(or(p, r), or(q, s)) [implies-intro(165-167)] | | | | | 169: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [implies-intro(168)] | | | | -------------------- | | | | 170: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(153, 154-161, 162-169)] | | | -------------------- | | | 171: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(133, 134-151, 152-170)] | | -------------------- | | 172: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(91, 92-131, 132-171)] | -------------------- | 173: implies(and(implies(p, q), implies(r, s)), implies(or(p, r), or(q, s))) [or-elim(1, 2-89, 90-172)]