let I, J be Program of SCMPDS ; :: thesis: Initialized I c= Initialized (stop (I ';' J))
set SA0 = Start-At (inspos 0 );
set IS = I ';' (J ';' (Stop SCMPDS ));
set Ip = Initialized (stop (I ';' J));
A1: dom (I ';' (J ';' (Stop SCMPDS ))) misses dom (Start-At (inspos 0 )) by SCMPDS_4:54;
Initialized (stop (I ';' J)) = (I ';' (J ';' (Stop SCMPDS ))) +* (Start-At (inspos 0 )) by SCMPDS_4:46;
then A2: I ';' (J ';' (Stop SCMPDS )) c= Initialized (stop (I ';' J)) by A1, FUNCT_4:33;
I c= I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:40;
then A3: I c= Initialized (stop (I ';' J)) by A2, XBOOLE_1:1;
A4: Start-At (inspos 0 ) c= Initialized (stop (I ';' J)) by FUNCT_4:26;
dom I misses dom (Start-At (inspos 0 )) by SCMPDS_4:54;
then I \/ (Start-At (inspos 0 )) = Initialized I by FUNCT_4:32;
hence Initialized I c= Initialized (stop (I ';' J)) by A3, A4, XBOOLE_1:8; :: thesis: verum