| | 1 | #u abandali |
| | 2 | #a h02 |
| | 3 | |
| | 4 | #q q04d |
| | 5 | |
| | 6 | p <=> q, p & q <=> (p | q) |
| | 7 | |
| | 8 | #check TP |
| | 9 | |
| | 10 | p <=> q <-> p & q <=> (p | q) |
| | 11 | |
| | 12 | 1) p & q <=> (p | q) |
| | 13 | 2) (p & q => p | q) & (p | q => p & q) by equiv |
| | 14 | 3) (!(p & q) | p | q) & (!(p | q) | p & q) by impl * 2 |
| | 15 | 4) (!p | !q | p | q) & (!(p | q) | p & q) by dm |
| | 16 | 5) (true | !q | q) & (!(p | q) | p & q) by lem |
| | 17 | 6) true & (!(p | q) | p & q) by simp1 |
| | 18 | 7) !(p | q) | p & q by simp1 |
| | 19 | 8) !p & !q | p & q by dm |
| | 20 | 9) (!p & !q | p) & (!p & !q | q) by distr |
| | 21 | 10) (!p | p) & (!q | p) & (!p | q) & (!q | q) by distr * 2 |
| | 22 | 11) true & (!q | p) & (!p | q) & true by lem * 2 |
| | 23 | 12) (!q | p) & (!p | q) by simp1 * 2 |
| | 24 | 13) (q => p) & (p => q) by impl * 2 |
| | 25 | 14) p <=> q by equiv |
projects / ~bandali / bndl.org / blame_incremental