let i be Instruction of SCM+FSA; :: thesis: for s being State of SCM+FSA holds
( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = (IC s) + 1 )
let s be State of SCM+FSA; :: thesis: ( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = (IC s) + 1 )
assume A1: not InsCode i in {0,6,7,8} ; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1
then A2: ( InsCode i <> 0 & InsCode i <> 6 ) by ENUMSET1:def 2;
A3: ( InsCode i <> 7 & InsCode i <> 8 ) by A1, ENUMSET1:def 2;
not not InsCode i = 0 & ... & not InsCode i = 12 by SCMFSA_2:16;

per cases then ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A2, A3;

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

then ex a, b being Int-Location st i = a := b by SCMFSA_2:30;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:63; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:31;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:64; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:32;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:65; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:33;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:66; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:34;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:67; :: thesis: verum

end;

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

then ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) by SCMFSA_2:38;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:72; :: thesis: verum

end;

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

then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:73; :: thesis: verum

end;

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

then ex a being Int-Location ex f being FinSeq-Location st i = a :=len f by SCMFSA_2:40;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:74; :: thesis: verum

end;

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

then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41;
hence (Exec (i,s)) . (IC ) = (IC s) + 1 by SCMFSA_2:75; :: thesis: verum

end;

end;