let N be with_non-empty_elements set ; :: thesis: for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = succ (IC s)
let i be Instruction of (STC N); :: thesis: for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = succ (IC s)
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies (Exec i,s) . (IC (STC N)) = succ (IC s) )
assume A1: InsCode i = 1 ; :: thesis: (Exec i,s) . (IC (STC N)) = succ (IC s)
set M = STC N;
A2: ( the Instruction-Counter of (STC N) = NAT & the Instructions of (STC N) = {[1,0 ],[0 ,0 ]} ) by Def11;
consider f being Function of (product the Object-Kind of (STC N)),(product the Object-Kind of (STC N)) such that
A3: for s being Element of product the Object-Kind of (STC N) holds f . s = s +* (NAT .--> (succ (s . NAT ))) and
A4: the Execution of (STC N) = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) by Def11;
( i = [1,0 ] or i = [0 ,0 ] ) by A2, TARSKI:def 2;
then A5: i in {[1,0 ]} by A1, MCART_1:7, TARSKI:def 1;

A6: now

assume i in {[0 ,0 ]} ; :: thesis: contradiction
then i = [0 ,0 ] by TARSKI:def 1;
hence contradiction by A1, MCART_1:7; :: thesis: verum

end;

dom ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) = {[0 ,0 ]} by FUNCOP_1:19;
then A7: the Execution of (STC N) . i = ([1,0 ] .--> f) . i by A4, A6, FUNCT_4:12
.= f by A5, FUNCOP_1:13 ;
A8: NAT in {NAT } by TARSKI:def 1;
then A9: NAT in dom (NAT .--> (succ (s . NAT ))) by FUNCOP_1:19;
thus (Exec i,s) . (IC (STC N)) = (s +* (NAT .--> (succ (s . NAT )))) . NAT by A2, A3, A7
.= (NAT .--> (succ (s . NAT ))) . NAT by A9, FUNCT_4:14
.= succ (IC s) by A2, A8, FUNCOP_1:13 ; :: thesis: verum