let i be Instruction of SCMPDS; :: thesis: for s being State of SCMPDS holds

( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = (IC s) + 1 )

let s be State of SCMPDS; :: thesis: ( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = (IC s) + 1 )

assume A1: not InsCode i in {0,1,4,5,6,14} ; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

A2: not not InsCode i = 0 & ... & not InsCode i = 14 by SCMPDS_2:6;

( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = (IC s) + 1 )

let s be State of SCMPDS; :: thesis: ( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = (IC s) + 1 )

assume A1: not InsCode i in {0,1,4,5,6,14} ; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

A2: not not InsCode i = 0 & ... & not InsCode i = 14 by SCMPDS_2:6;

per cases
( InsCode i = 2 or InsCode i = 3 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 )
by A2, A1, ENUMSET1:def 4;

end;

suppose
InsCode i = 2
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a being Int_position ex k1 being Integer st i = a := k1
by SCMPDS_2:28;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:45; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:45; :: thesis: verum

suppose
InsCode i = 3
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a being Int_position ex k1 being Integer st i = saveIC (a,k1)
by SCMPDS_2:29;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:59; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:59; :: thesis: verum

suppose
InsCode i = 7
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a being Int_position ex k1, k2 being Integer st i = (a,k1) := k2
by SCMPDS_2:33;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:46; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:46; :: thesis: verum

suppose
InsCode i = 8
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a being Int_position ex k1, k2 being Integer st i = AddTo (a,k1,k2)
by SCMPDS_2:34;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:48; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:48; :: thesis: verum

suppose
InsCode i = 9
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a, b being Int_position ex k1, k2 being Integer st i = AddTo (a,k1,b,k2)
by SCMPDS_2:35;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:49; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:49; :: thesis: verum

suppose
InsCode i = 10
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a, b being Int_position ex k1, k2 being Integer st i = SubFrom (a,k1,b,k2)
by SCMPDS_2:36;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:50; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:50; :: thesis: verum

suppose
InsCode i = 11
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a, b being Int_position ex k1, k2 being Integer st i = MultBy (a,k1,b,k2)
by SCMPDS_2:37;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:51; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:51; :: thesis: verum

suppose
InsCode i = 12
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a, b being Int_position ex k1, k2 being Integer st i = Divide (a,k1,b,k2)
by SCMPDS_2:38;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:52; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:52; :: thesis: verum

suppose
InsCode i = 13
; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

then
ex a, b being Int_position ex k1, k2 being Integer st i = (a,k1) := (b,k2)
by SCMPDS_2:39;

hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:47; :: thesis: verum

end;hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMPDS_2:47; :: thesis: verum