Prove the following using our axiomatic scheme.
{ i * k = n AND k mod 2 = 0 } k := k / 2; i := i * 2; {i * k = n }
1. i * k = n AND k mod 2 = 0 implies (i * 2) * (k / 2) = n (Math fact) 2. { i * k = n AND k mod 2 = 0 } (Conseq: 1) { (i * 2) * (k / 2) = n } 3. { (i * 2) * (k / 2) = n } (Assignment) k := k / 2; { (i * 2) * k = n } 4. { i * k = n AND k mod 2 = 0 } (Seq: 2, 3) k := k / 2; { (i * 2) * k = n } 5. { (i * 2) * k = n } (Assignment) i := i * 2; {i * k = n } 6. { i * k = n AND k mod 2 = 0 } (Seq: 4, 5) k := k / 2; i := i * 2; {i * k = n }