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 ) = succ (IC s) )
let s be State of SCM+FSA; :: thesis: ( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = succ (IC s) )
A1: InsCode i <= 12 by SCMFSA_2:16;
assume A4: not InsCode i in {0,6,7,8} ; :: thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then A5: ( InsCode i <> 0 & InsCode i <> 6 ) by ENUMSET1:def 2;
A6: ( InsCode i <> 7 & InsCode i <> 8 ) by A4, ENUMSET1:def 2;

per cases ( 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 A5, A6, A1, NAT_1:36;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;