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