let s be State of SCMPDS; :: thesis: for I being Instruction of SCMPDS st InsCode I = 0 holds
Exec (I,s) = s
let I be Instruction of SCMPDS; :: thesis: ( InsCode I = 0 implies Exec (I,s) = s )
assume InsCode I = 0 ; :: thesis: Exec (I,s) = s
then A1: ( InsCode I <> 1 & InsCode I <> 2 & InsCode I <> 3 & InsCode I <> 4 & InsCode I <> 5 & InsCode I <> 6 & InsCode I <> 7 & InsCode I <> 8 & InsCode I <> 9 & InsCode I <> 10 & InsCode I <> 11 & InsCode I <> 12 & InsCode I <> 13 & InsCode I <> 14 ) ;
reconsider ss = s as SCM-State by CARD_3:107;
reconsider ii = I as Element of SCMPDS-Instr ;
thus Exec (I,s) = ( the Execution of SCMPDS . I) . s
.= (SCMPDS-Exec . I) . s
.= SCM-Exec-Res (ii,ss) by SCMPDS_1:def 23
.= s by A1, SCMPDS_1:def 22 ; :: thesis: verum