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 SCM+FSA) = succ (IC s) )
let s be State of SCM+FSA; :: thesis: ( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) )
A1: InsCode i <= 11 + 1 by SCMFSA_2:35;
A2: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A3: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
assume A4: not InsCode i in {0,6,7,8} ; :: thesis: (Exec (i,s)) . (IC SCM+FSA) = 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, A2, A3, NAT_1:8, NAT_1:33;

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

then ex a, b being Int-Location st i = a := b by SCMFSA_2:54;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:89; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:55;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:90; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:56;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:91; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:57;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:92; :: thesis: verum

end;

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

then ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:58;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:93; :: thesis: verum

end;

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

then ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) by SCMFSA_2:62;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:98; :: thesis: verum

end;

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

then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:63;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:99; :: thesis: verum

end;

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

then ex a being Int-Location ex f being FinSeq-Location st i = a :=len f by SCMFSA_2:64;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:100; :: thesis: verum

end;

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

then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:65;
hence (Exec (i,s)) . (IC SCM+FSA) = succ (IC s) by SCMFSA_2:101; :: thesis: verum

end;

end;