let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds (Initialized s) +* (Initialized I) = s +* (Initialized I)
let I be Program of SCMPDS ; :: thesis: (Initialized s) +* (Initialized I) = s +* (Initialized I)
set SA0 = Start-At (inspos 0 );
A1: dom I misses dom (Start-At (inspos 0 )) by SCMPDS_4:54;
thus (Initialized s) +* (Initialized I) = (s +* (Start-At (inspos 0 ))) +* (Initialized I) by SCMPDS_5:def 4
.= (s +* (Start-At (inspos 0 ))) +* (I +* (Start-At (inspos 0 ))) by SCMPDS_4:def 2
.= ((s +* (Start-At (inspos 0 ))) +* I) +* (Start-At (inspos 0 )) by FUNCT_4:15
.= (s +* ((Start-At (inspos 0 )) +* I)) +* (Start-At (inspos 0 )) by FUNCT_4:15
.= (s +* (I +* (Start-At (inspos 0 )))) +* (Start-At (inspos 0 )) by A1, FUNCT_4:36
.= ((s +* I) +* (Start-At (inspos 0 ))) +* (Start-At (inspos 0 )) by FUNCT_4:15
.= (s +* I) +* ((Start-At (inspos 0 )) +* (Start-At (inspos 0 ))) by FUNCT_4:15
.= s +* (I +* (Start-At (inspos 0 ))) by FUNCT_4:15
.= s +* (Initialized I) by SCMPDS_4:def 2 ; :: thesis: verum