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 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 s) + 1

let s be State of (STC N); :: thesis: ( InsCode i = 1 implies (Exec (i,s)) . () = (IC s) + 1 )
set M = STC N;
assume A1: InsCode i = 1 ; :: thesis: (Exec (i,s)) . () = (IC s) + 1
A2: now :: thesis: not i in {[0,0,0]}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 ;
A4: 0 in 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
.= by Def7 ;
then A11: 0 in dom (the_Values_of (STC N)) by TARSKI:def 1;
Values () = NAT by MEMSTR_0:def 6;
then reconsider k = s . 0 as Element of NAT by ;
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
.= f by ;
hence (Exec (i,s)) . () = (s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . 0 by A9, A8
.= (0 .--> ((In ((s . 0),NAT)) + 1)) . 0 by
.= (In (k,NAT)) + 1 by
.= (IC s) + 1 by A9 ;
:: thesis: verum