435 Let x and y be natural variables. Rewrite the following program as a program that does notuse ||.
(a) §
(b) §
x:= x+1 || if x=0 then y:= 1 else ok fi
x:= x+1 || if x=0 then y:= 1 else ok fi
= xʹ′ = x+1 || if x=0 then yʹ′=1 else yʹ′=y fi
= xʹ′ = x+1 ∧ if x=0 then yʹ′=1 else yʹ′=y fi
= if x=0 then xʹ′ = x+1 ∧ yʹ′=1 else xʹ′ = x+1 ∧ yʹ′=y fi
= if x=0 then y:= 1. xʹ′ = x+1 ∧ yʹ′=y else ok. xʹ′ = x+1 ∧ yʹ′=y fi
= if x=0 then y:= 1. x:= x+1 else ok. x:= x+1 fi
= if x=0 then y:= 1 else ok fi. x:= x+1
ifx>0theny:=x–1elseokfi || ifx=0thenx:=y+1elseokfi
ifx>0theny:=x–1elseokfi || ifx=0thenx:=y+1elseokfi
= if x>0 then yʹ′ = x–1 else yʹ′=y fi || if x=0 then xʹ′ = y+1 else xʹ′=x fi
= ifx>0thenyʹ′=x–1elseyʹ′=yfi ∧ ifx=0thenxʹ′=y+1elsexʹ′=xfi
= if x>0 then yʹ′ = x–1 else yʹ′=y fi ∧ if ¬(x>0) then xʹ′ = y+1 else xʹ′=x fi case revers.
= if x>0 then yʹ′ = x–1 else yʹ′=y fi ∧ if x>0 then xʹ′=x else xʹ′=y+1 fi case distributive
= if x>0 then yʹ′ = x–1 ∧ xʹ′=x else xʹ′=y+1 ∧ yʹ′=y fi assignment twice
= if x>0 then y:= x–1 else x:= y+1 fi
expand assignments and ok independent composition distribution substitution law and identity assignment distribution
asmtsand ok indep. comp. x isnatural