let n be Nat; :: thesis: for s being State of SCM
for P being Instruction-Sequence of SCM
for I being sequential Instruction of SCM st CurInstr (P,(Comput (P,s,n))) = I & IC (Comput (P,s,n)) in dom P holds
IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1
let s be State of SCM; :: thesis: for P being Instruction-Sequence of SCM
for I being sequential Instruction of SCM st CurInstr (P,(Comput (P,s,n))) = I & IC (Comput (P,s,n)) in dom P holds
IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1
let P be Instruction-Sequence of SCM; :: thesis: for I being sequential Instruction of SCM st CurInstr (P,(Comput (P,s,n))) = I & IC (Comput (P,s,n)) in dom P holds
IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1
let I be sequential Instruction of SCM; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = I & IC (Comput (P,s,n)) in dom P implies IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 )
set t = Comput (P,s,n);
assume A1: CurInstr (P,(Comput (P,s,n))) = I ; :: thesis: ( not IC (Comput (P,s,n)) in dom P or IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 )
assume IC (Comput (P,s,n)) in dom P ; :: thesis: IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1
then A2: P . (IC (Comput (P,s,n))) = I by A1, PARTFUN1:def 6;
Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3;
hence IC (Comput (P,s,(n + 1))) = (Exec ((P . (IC (Comput (P,s,n)))),(Comput (P,s,n)))) . (IC ) by EXTPRO_1:28
.= (IC (Comput (P,s,n))) + 1 by A2, AMISTD_1:def 8 ;
:: thesis: verum