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

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))

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

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]}

the InstructionsF of (STC N) = {[1,{},{}],[0,{},{}]}
by Def7;assume
i in {[0,0,0]}
; :: thesis: contradiction

then i = [0,0,0] by TARSKI:def 1;

hence contradiction by A1; :: thesis: verum

end;then i = [0,0,0] by TARSKI:def 1;

hence contradiction by A1; :: thesis: verum

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

A9:
IC = 0
by Def7;
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;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

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