theorem
for
U1,
U2 being
preIfWhileAlgebra st
UAStr(# the
carrier of
U1, the
charact of
U1 #)
= UAStr(# the
carrier of
U2, the
charact of
U2 #) holds
(
EmptyIns U1 = EmptyIns U2 & ( for
I1,
J1 being
Element of
U1 for
I2,
J2 being
Element of
U2 st
I1 = I2 &
J1 = J2 holds
(
I1 \; J1 = I2 \; J2 &
while (
I1,
J1)
= while (
I2,
J2) & ( for
C1 being
Element of
U1 for
C2 being
Element of
U2 st
C1 = C2 holds
if-then-else (
C1,
I1,
J1)
= if-then-else (
C2,
I2,
J2) ) ) ) ) ;