Description: CONTRADICTION PROVED AT 1 + 1 = 2 .
Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses.
Note: Values that when added would exceed a 4bit value are not supported.
Note: Digits begin from left (least) to right (greatest). E.g., 1000 would be '1', 0100 would be '2', 0010 would be '4'.
How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit.
( et <-> F ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. (Contributed by Jarvin Udandy, 6-Sep-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dandysum2p2e4.a | |- ( ph <-> ( th /\ ta ) ) |
|
| dandysum2p2e4.b | |- ( ps <-> ( et /\ ze ) ) |
||
| dandysum2p2e4.c | |- ( ch <-> ( si /\ rh ) ) |
||
| dandysum2p2e4.d | |- ( th <-> F. ) |
||
| dandysum2p2e4.e | |- ( ta <-> F. ) |
||
| dandysum2p2e4.f | |- ( et <-> T. ) |
||
| dandysum2p2e4.g | |- ( ze <-> T. ) |
||
| dandysum2p2e4.h | |- ( si <-> F. ) |
||
| dandysum2p2e4.i | |- ( rh <-> F. ) |
||
| dandysum2p2e4.j | |- ( mu <-> F. ) |
||
| dandysum2p2e4.k | |- ( la <-> F. ) |
||
| dandysum2p2e4.l | |- ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) |
||
| dandysum2p2e4.m | |- ( jph <-> ( ( et \/_ ze ) \/ ph ) ) |
||
| dandysum2p2e4.n | |- ( jps <-> ( ( si \/_ rh ) \/ ps ) ) |
||
| dandysum2p2e4.o | |- ( jch <-> ( ( mu \/_ la ) \/ ch ) ) |
||
| Assertion | dandysum2p2e4 | |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph <-> ( th /\ ta ) ) /\ ( ps <-> ( et /\ ze ) ) ) /\ ( ch <-> ( si /\ rh ) ) ) /\ ( th <-> F. ) ) /\ ( ta <-> F. ) ) /\ ( et <-> T. ) ) /\ ( ze <-> T. ) ) /\ ( si <-> F. ) ) /\ ( rh <-> F. ) ) /\ ( mu <-> F. ) ) /\ ( la <-> F. ) ) /\ ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) ) /\ ( jph <-> ( ( et \/_ ze ) \/ ph ) ) ) /\ ( jps <-> ( ( si \/_ rh ) \/ ps ) ) ) /\ ( jch <-> ( ( mu \/_ la ) \/ ch ) ) ) -> ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dandysum2p2e4.a | |- ( ph <-> ( th /\ ta ) ) |
|
| 2 | dandysum2p2e4.b | |- ( ps <-> ( et /\ ze ) ) |
|
| 3 | dandysum2p2e4.c | |- ( ch <-> ( si /\ rh ) ) |
|
| 4 | dandysum2p2e4.d | |- ( th <-> F. ) |
|
| 5 | dandysum2p2e4.e | |- ( ta <-> F. ) |
|
| 6 | dandysum2p2e4.f | |- ( et <-> T. ) |
|
| 7 | dandysum2p2e4.g | |- ( ze <-> T. ) |
|
| 8 | dandysum2p2e4.h | |- ( si <-> F. ) |
|
| 9 | dandysum2p2e4.i | |- ( rh <-> F. ) |
|
| 10 | dandysum2p2e4.j | |- ( mu <-> F. ) |
|
| 11 | dandysum2p2e4.k | |- ( la <-> F. ) |
|
| 12 | dandysum2p2e4.l | |- ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) |
|
| 13 | dandysum2p2e4.m | |- ( jph <-> ( ( et \/_ ze ) \/ ph ) ) |
|
| 14 | dandysum2p2e4.n | |- ( jps <-> ( ( si \/_ rh ) \/ ps ) ) |
|
| 15 | dandysum2p2e4.o | |- ( jch <-> ( ( mu \/_ la ) \/ ch ) ) |
|
| 16 | 12 | biimpi | |- ( ka -> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) |
| 17 | 4 5 | bothfbothsame | |- ( th <-> ta ) |
| 18 | 17 | aisbnaxb | |- -. ( th \/_ ta ) |
| 19 | 4 | aisfina | |- -. th |
| 20 | 19 | notatnand | |- -. ( th /\ ta ) |
| 21 | 18 20 | 2false | |- ( ( th \/_ ta ) <-> ( th /\ ta ) ) |
| 22 | 21 | aisbnaxb | |- -. ( ( th \/_ ta ) \/_ ( th /\ ta ) ) |
| 23 | 16 22 | aibnbaif | |- ( ka <-> F. ) |
| 24 | 13 | biimpi | |- ( jph -> ( ( et \/_ ze ) \/ ph ) ) |
| 25 | 6 7 | bothtbothsame | |- ( et <-> ze ) |
| 26 | 25 | aisbnaxb | |- -. ( et \/_ ze ) |
| 27 | 20 1 | mtbir | |- -. ph |
| 28 | 26 27 | pm3.2ni | |- -. ( ( et \/_ ze ) \/ ph ) |
| 29 | 24 28 | aibnbaif | |- ( jph <-> F. ) |
| 30 | 23 29 | pm3.2i | |- ( ( ka <-> F. ) /\ ( jph <-> F. ) ) |
| 31 | 6 7 | astbstanbst | |- ( ( et /\ ze ) <-> T. ) |
| 32 | 2 31 | aiffbbtat | |- ( ps <-> T. ) |
| 33 | 32 | aistia | |- ps |
| 34 | 33 | olci | |- ( ( si \/_ rh ) \/ ps ) |
| 35 | 34 | bitru | |- ( ( ( si \/_ rh ) \/ ps ) <-> T. ) |
| 36 | 14 35 | aiffbbtat | |- ( jps <-> T. ) |
| 37 | 30 36 | pm3.2i | |- ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) |
| 38 | 15 | biimpi | |- ( jch -> ( ( mu \/_ la ) \/ ch ) ) |
| 39 | 10 11 | bothfbothsame | |- ( mu <-> la ) |
| 40 | 39 | aisbnaxb | |- -. ( mu \/_ la ) |
| 41 | 8 | aisfina | |- -. si |
| 42 | 41 | notatnand | |- -. ( si /\ rh ) |
| 43 | 42 3 | mtbir | |- -. ch |
| 44 | 40 43 | pm3.2ni | |- -. ( ( mu \/_ la ) \/ ch ) |
| 45 | 38 44 | aibnbaif | |- ( jch <-> F. ) |
| 46 | 37 45 | pm3.2i | |- ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) |
| 47 | 46 | a1i | |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph <-> ( th /\ ta ) ) /\ ( ps <-> ( et /\ ze ) ) ) /\ ( ch <-> ( si /\ rh ) ) ) /\ ( th <-> F. ) ) /\ ( ta <-> F. ) ) /\ ( et <-> T. ) ) /\ ( ze <-> T. ) ) /\ ( si <-> F. ) ) /\ ( rh <-> F. ) ) /\ ( mu <-> F. ) ) /\ ( la <-> F. ) ) /\ ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) ) /\ ( jph <-> ( ( et \/_ ze ) \/ ph ) ) ) /\ ( jps <-> ( ( si \/_ rh ) \/ ps ) ) ) /\ ( jch <-> ( ( mu \/_ la ) \/ ch ) ) ) -> ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) ) |