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 ) = succ (IC s) )
let s be State of SCMPDS; :: thesis: ( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = succ (IC s) )
assume A1: not InsCode i in {0,1,4,5,6,14} ; :: thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then A2: ( InsCode i <> 0 & InsCode i <> 1 ) by ENUMSET1:def 4;
A3: InsCode i <> 6 by A1, ENUMSET1:def 4;
A4: ( InsCode i <> 4 & InsCode i <> 5 ) by A1, ENUMSET1:def 4;
InsCode i <> 14 by A1, ENUMSET1:def 4;

per cases then ( 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:60, SCMPDS_2:6;

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

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

end;

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

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

end;

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

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 ) = succ (IC s) by SCMPDS_2:46; :: thesis: verum

end;

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

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 ) = succ (IC s) by SCMPDS_2:48; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: (Exec (i,s)) . (IC ) = 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:35;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:49; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: (Exec (i,s)) . (IC ) = 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:36;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:50; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: (Exec (i,s)) . (IC ) = 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:37;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:51; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: (Exec (i,s)) . (IC ) = 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:38;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:52; :: thesis: verum

end;

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

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 ) = succ (IC s) by SCMPDS_2:47; :: thesis: verum

end;

end;