let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
( Initialized I c= s +* (I +* (Initialize ((intloc 0) .--> 1))) & s +* (I +* (Initialize ((intloc 0) .--> 1))) = s +* I & (s +* (I +* (Initialize ((intloc 0) .--> 1)))) +* (Directed I) = s +* (Directed I) )
let s be State of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies ( Initialized I c= s +* (I +* (Initialize ((intloc 0) .--> 1))) & s +* (I +* (Initialize ((intloc 0) .--> 1))) = s +* I & (s +* (I +* (Initialize ((intloc 0) .--> 1)))) +* (Directed I) = s +* (Directed I) ) )
assume A1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( Initialized I c= s +* (I +* (Initialize ((intloc 0) .--> 1))) & s +* (I +* (Initialize ((intloc 0) .--> 1))) = s +* I & (s +* (I +* (Initialize ((intloc 0) .--> 1)))) +* (Directed I) = s +* (Directed I) )
set sISA0 = s +* (I +* (Initialize ((intloc 0) .--> 1)));
I +* (Initialize ((intloc 0) .--> 1)) c= s +* (I +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:26;
hence Initialized I c= s +* (I +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15; :: thesis: ( s +* (I +* (Initialize ((intloc 0) .--> 1))) = s +* I & (s +* (I +* (Initialize ((intloc 0) .--> 1)))) +* (Directed I) = s +* (Directed I) )
thus s +* (I +* (Initialize ((intloc 0) .--> 1))) = (s +* I) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= (s +* (Initialize ((intloc 0) .--> 1))) +* I by Th19
.= s +* I by A1, FUNCT_4:79 ; :: thesis: (s +* (I +* (Initialize ((intloc 0) .--> 1)))) +* (Directed I) = s +* (Directed I)
A2: dom (Directed I) = dom I by FUNCT_4:105;
thus (s +* (I +* (Initialize ((intloc 0) .--> 1)))) +* (Directed I) = ((s +* I) +* (Initialize ((intloc 0) .--> 1))) +* (Directed I) by FUNCT_4:15
.= ((s +* (Initialize ((intloc 0) .--> 1))) +* I) +* (Directed I) by Th19
.= (s +* I) +* (Directed I) by A1, FUNCT_4:79
.= s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A2, FUNCT_4:20 ; :: thesis: verum