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