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