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)

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

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

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

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;

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

A7:
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 A4;

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 A4;

hence f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ; :: thesis: verum

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