let N be non empty 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) )
set M = STC N;
assume A1: InsCode i = 1 ; :: thesis: (Exec (i,s)) . (IC (STC N)) = succ (IC s)

A2: now

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

end;

the Instructions of (STC N) = {[1,0,0],[0,0,0]} by AMISTD_1:def 11;
then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def 2;
then A3: i in {[1,0,0]} by A1, RECDEF_2:def 1, TARSKI:def 1;
A4: NAT in {NAT} by TARSKI:def 1;
then A5: NAT in dom (NAT .--> (succ (s . NAT))) by FUNCOP_1:19;
consider f being Function of (product the Object-Kind of (STC N)),(product the Object-Kind of (STC N)) such that
A6: for s being Element of product the Object-Kind of (STC N) holds f . s = s +* (NAT .--> (succ (s . NAT))) and
A7: the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) by AMISTD_1:def 11;
B6: for s being State of (STC N) holds f . s = s +* (NAT .--> (succ (s . NAT)))

proof

let s be State of (STC N); :: thesis: f . s = s +* (NAT .--> (succ (s . NAT)))
reconsider s = s as Element of product the Object-Kind of (STC N) by PBOOLE:155;
f . s = s +* (NAT .--> (succ (s . NAT))) by A6;
hence f . s = s +* (NAT .--> (succ (s . NAT))) ; :: thesis: verum

end;

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