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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
end;