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 ]} ; :: thesis: contradiction
then i = [0 ,0 ] by TARSKI:def 1;
hence contradiction by A1, MCART_1:7; :: thesis: verum

end;

the Instructions of (STC N) = {[1,0 ],[0 ,0 ]} by Def11;
then ( i = [1,0 ] or i = [0 ,0 ] ) by TARSKI:def 2;
then A3: i in {[1,0 ]} by A1, MCART_1:7, 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 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) by Def11;
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 Def11;
dom ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) = {[0 ,0 ]} by FUNCOP_1:19;
then the Execution of (STC N) . i = ([1,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