| FALSE : | a3 = 0 | |
|
| IMP : | a1 → a3 ≡{a3′ = a
1 + a3 = a1} | |
|
| FALSE : | a4 = 0 | |
|
| IMP : | a2 → a4 ≡{a4′ = a
2 + a4 = a2} | |
|
| IMP : | a3 → a4 ≡{a4′ = a
3 + a4 = a1 + a2} | |
|
| FALSE : | a5 = 0 | |
|
| IMP : | a4 → a5 ≡{a5′ = a
4 + a5 = a1.a2} | |
|
| FALSE : | a4 = 0 | |
|
| IMP : | a2 → a4 ≡{a4′ = a
2 + a4 = a2} | |
|
| IMP : | a4 → a3 ≡{a3′ = a
4 + a3 = a2 + a1} | |
|
| IMP : | a3 → a5 ≡{a5′ = a
3 + a5 = a2.a1 + a1.a2 ≡ a1 XOR a2} | |
|
| IMP : | a1 → a4 ≡{a4′ = a
1 + a4 = a1 + a2} | |
|
| FALSE : | a1 = 0 | |
|
| IMP : | a5 → a1 ≡{a1′ = a
5 + a1 = a1 XOR a2} | |
|
| IMP : | cin → a1 ≡{a1′ = c
in + a1 = cin + a1 XOR a2} | |
|
| FALSE : | a2 = 0 | |
|
| IMP : | a1 → a2 ≡{a1′ = a
1 + a2 = cin.(a1 XOR a2)} | |
|
| IMP : | a4 → a2 ≡{a4′ = a
4 + a2 = (a1.a2) + cin.(a1 XOR a2) ≡ cout} | |
|
| |
|
| FALSE : | a3 = 0 | |
|
| IMP : | cin → a3 ≡{a3′ = c
in + a3 = cin} | |
|
| FALSE : | a1 = 0 | |
|
| IMP : | a5 → a1 ≡{a1′ = a
5 + a1 = a1 XOR a2} | |
|
| IMP : | a3 → a1 ≡{a1′ = a
3 + a1 = cin + a1 XOR a2} | |
|
| FALSE : | a3 = 0 | |
|
| IMP : | a1 → a3 ≡{a3′ = a
1 + a3 = cin.(a1 XOR a2)} | |
|
| IMP : | cin → a5 ≡{a5′ = c
in + a5 = cin + a1 XOR a2 | |
|
| IMP : | a5 → a3 ≡{a5′ = a
5 + a3 = cin.(a1 XOR a2) + cin.(a1 XOR a2)} | |
|
| |
|
| ≡{a5′ = c
in XOR a1 XOR a2 ≡ s} | (A.4) |