let N be with_zero 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 ) = (IC s) + 1
let i be Instruction of (STC N); :: thesis: for s being State of (STC N) st InsCode i = 1 holds
(Exec (i,s)) . (IC ) = (IC s) + 1
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies (Exec (i,s)) . (IC ) = (IC s) + 1 )
set M = STC N;
assume A1: InsCode i = 1 ; :: thesis: (Exec (i,s)) . (IC ) = (IC s) + 1

A2: now :: thesis: not i in {[0,0,0]}

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

end;

the InstructionsF of (STC N) = {[1,{},{}],[0,{},{}]} by Def7;
then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def 2;
then A3: i in {[1,0,0]} by A1, TARSKI:def 1;
A4: 0 in {0} by TARSKI:def 1;
then A5: 0 in dom (0 .--> ((In ((s . 0),NAT)) + 1)) ;
consider f being Function of (product (the_Values_of (STC N))),(product (the_Values_of (STC N))) such that
A6: for s being Element of product (the_Values_of (STC N)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) and
A7: the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of (STC N))))) by Def7;
A8: for s being State of (STC N) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1))

proof

let s be State of (STC N); :: thesis: f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1))
reconsider s = s as Element of product (the_Values_of (STC N)) by CARD_3:107;
f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) by A6;
hence f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ; :: thesis: verum

end;

A9: IC = 0 by Def7;
A10: s in product (the_Values_of (STC N)) by CARD_3:107;
dom (the_Values_of (STC N)) = the carrier of (STC N) by PARTFUN1:def 2
.= {0} by Def7 ;
then A11: 0 in dom (the_Values_of (STC N)) by TARSKI:def 1;
Values (IC ) = NAT by MEMSTR_0:def 6;
then reconsider k = s . 0 as Element of NAT by A10, A11, CARD_3:9, A9;
dom ([0,0,0] .--> (id (product (the_Values_of (STC N))))) = {[0,0,0]} ;
then the Execution of (STC N) . i = ([1,0,0] .--> f) . i by A7, A2, FUNCT_4:11
.= f by A3, FUNCOP_1:7 ;
hence (Exec (i,s)) . (IC ) = (s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . 0 by A9, A8
.= (0 .--> ((In ((s . 0),NAT)) + 1)) . 0 by A5, FUNCT_4:13
.= (In (k,NAT)) + 1 by A4, FUNCOP_1:7
.= (IC s) + 1 by A9 ;
:: thesis: verum