let s be State of ; :: thesis: for I being Program of
for n being Element of NAT st IC (Computation (s +* (Initialized I)),n) = inspos 0 holds
(Computation (s +* (Initialized I)),n) +* (Initialized I) = Computation (s +* (Initialized I)),n
let I be Program of ; :: thesis: for n being Element of NAT st IC (Computation (s +* (Initialized I)),n) = inspos 0 holds
(Computation (s +* (Initialized I)),n) +* (Initialized I) = Computation (s +* (Initialized I)),n
let n be Element of NAT ; :: thesis: ( IC (Computation (s +* (Initialized I)),n) = inspos 0 implies (Computation (s +* (Initialized I)),n) +* (Initialized I) = Computation (s +* (Initialized I)),n )
set II = Initialized I;
set sn = Computation (s +* (Initialized I)),n;
A1: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
I c= I +* (Start-At (inspos 0 )) by SCMPDS_6:6;
then I c= s +* (Initialized I) by A1, XBOOLE_1:1;
then A2: I c= Computation (s +* (Initialized I)),n by AMI_1:81;
assume IC (Computation (s +* (Initialized I)),n) = inspos 0 ; :: thesis: (Computation (s +* (Initialized I)),n) +* (Initialized I) = Computation (s +* (Initialized I)),n
then (Computation (s +* (Initialized I)),n) +* (Initialized I) = (Computation (s +* (Initialized I)),n) +* I by Th5;
hence (Computation (s +* (Initialized I)),n) +* (Initialized I) = Computation (s +* (Initialized I)),n by A2, FUNCT_4:79; :: thesis: verum