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) = IncIC (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) = IncIC (s,1)
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies Exec (i,s) = IncIC (s,1) )
set M = STC N;
assume A1: InsCode i = 1 ; :: thesis: Exec (i,s) = IncIC (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;
consider f being Function of (product (the_Values_of (STC N))),(product (the_Values_of (STC N))) such that
A4: for s being Element of product (the_Values_of (STC N)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) and
A5: the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of (STC N))))) by Def7;
A6: 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 A4;
hence f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ; :: thesis: verum

end;

A7: IC = 0 by Def7;
A8: 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 A9: 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 A8, A9, CARD_3:9, A7;
A10: Start-At (((IC s) + 1),(STC N)) = 0 .--> ((In (k,NAT)) + 1) by A7;
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 A5, A2, FUNCT_4:11
.= f by A3, FUNCOP_1:7 ;
hence Exec (i,s) = IncIC (s,1) by A10, A6; :: thesis: verum