let i be Instruction of SCMPDS ; :: thesis: for s being State of SCMPDS holds
( InsCode i in {0 ,1,4,5,6} or (Exec i,s) . (IC SCMPDS ) = succ (IC s) )
let s be State of SCMPDS ; :: thesis: ( InsCode i in {0 ,1,4,5,6} or (Exec i,s) . (IC SCMPDS ) = succ (IC s) )
assume A1: not InsCode i in {0 ,1,4,5,6} ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)
then A2: ( InsCode i <> 0 & InsCode i <> 1 ) by ENUMSET1:def 3;
A3: InsCode i <> 6 by A1, ENUMSET1:def 3;
A4: ( InsCode i <> 4 & InsCode i <> 5 ) by A1, ENUMSET1:def 3;

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, A4, A3, NAT_1:38, SCMPDS_2:15;

suppose InsCode i = 2 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a being Int_position ex k1 being Integer st i = a := k1 by SCMPDS_2:37;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:57; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a being Int_position ex k1 being Integer st i = saveIC a,k1 by SCMPDS_2:38;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:71; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a being Int_position ex k1, k2 being Integer st i = a,k1 := k2 by SCMPDS_2:42;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:58; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a being Int_position ex k1, k2 being Integer st i = AddTo a,k1,k2 by SCMPDS_2:43;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:60; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a, b being Int_position ex k1, k2 being Integer st i = AddTo a,k1,b,k2 by SCMPDS_2:44;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:61; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a, b being Int_position ex k1, k2 being Integer st i = SubFrom a,k1,b,k2 by SCMPDS_2:45;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:62; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a, b being Int_position ex k1, k2 being Integer st i = MultBy a,k1,b,k2 by SCMPDS_2:46;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:63; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a, b being Int_position ex k1, k2 being Integer st i = Divide a,k1,b,k2 by SCMPDS_2:47;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:64; :: thesis: verum

end;

suppose InsCode i = 13 ; :: thesis: (Exec i,s) . (IC SCMPDS ) = succ (IC s)

then ex a, b being Int_position ex k1, k2 being Integer st i = a,k1 := b,k2 by SCMPDS_2:48;
hence (Exec i,s) . (IC SCMPDS ) = succ (IC s) by SCMPDS_2:59; :: thesis: verum

end;

end;