427 Let u be a binary user’s variable. Let a and b be old binary implementer’s variables. We replace a and b by new integer implementer’s variables x and y using the convention (from the C language) that 0 stands for ⊥ and non-zero integers stand for ⊤.
(a) What is the transformer? § a=(x⧧0) ∧ b=(y⧧0)
(b) Transform a:= ¬a .
§
∀a, b· a=(x⧧0) ∧ b=(y⧧0) ⇒ ∃aʹ, bʹ· aʹ=(xʹ⧧0) ∧ bʹ=(yʹ⧧0) ∧ (a:= ¬a)
= ∀a, b· a=(x⧧0) ∧ b=(y⧧0)
⇒ ∃aʹ, bʹ· aʹ=(xʹ⧧0) ∧ bʹ=(yʹ⧧0) ∧ aʹ=¬a ∧ bʹ=b ∧ uʹ=u
= ∀a, b· a=(x⧧0) ∧ b=(y⧧0) ⇒ ¬a=(xʹ⧧0) ∧ b=(yʹ⧧0) ∧ uʹ=u
= ¬(x⧧0)=(xʹ⧧0) ∧ (y⧧0)=(yʹ⧧0) ∧ uʹ=u
⇐ if x=0 then x:= 1 else x:= 0 fi
(c) Transform u:= a∧b .
§
∀a, b· a=(x⧧0) ∧ b=(y⧧0) ⇒ ∃aʹ, bʹ· aʹ=(xʹ⧧0) ∧ bʹ=(yʹ⧧0) ∧ (u:= a∧b) replace asmt
= ∀a, b· a=(x⧧0) ∧ b=(y⧧0)
⇒ ∃aʹ, bʹ· aʹ=(xʹ⧧0) ∧ bʹ=(yʹ⧧0) ∧ aʹ=a ∧ bʹ=b ∧ uʹ=a∧b 1-pt aʹ and bʹ
= ∀a, b· a=(x⧧0) ∧ b=(y⧧0) ⇒ a=(xʹ⧧0) ∧ b=(yʹ⧧0) ∧ uʹ=a∧b 1-pt a and b
= (x 0)=(xʹ⧧0) ∧ (y⧧0)=(yʹ⧧0) ∧ uʹ=(x⧧0)∧(y⧧0) ⇐ u:= (x⧧0)∧(y⧧0)
replace asmt 1-pt aʹ and bʹ
1-pt a and b