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