let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for il being Nat

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for il being Nat

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

let il be Nat; :: thesis: for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

let i be Instruction of S; :: thesis: ( i is sequential implies NIC (i,il) = {(il + 1)} )

assume A1: for s being State of S holds (Exec (i,s)) . (IC ) = (IC s) + 1 ; :: according to AMISTD_1:def 8 :: thesis: NIC (i,il) = {(il + 1)}

for il being Nat

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for il being Nat

for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

let il be Nat; :: thesis: for i being Instruction of S st i is sequential holds

NIC (i,il) = {(il + 1)}

let i be Instruction of S; :: thesis: ( i is sequential implies NIC (i,il) = {(il + 1)} )

assume A1: for s being State of S holds (Exec (i,s)) . (IC ) = (IC s) + 1 ; :: according to AMISTD_1:def 8 :: thesis: NIC (i,il) = {(il + 1)}

now :: thesis: for x being object holds

( x in {(il + 1)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

hence
NIC (i,il) = {(il + 1)}
by TARSKI:2; :: thesis: verum( x in {(il + 1)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

let x be object ; :: thesis: ( x in {(il + 1)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

end;A2: now :: thesis: ( x = il + 1 implies x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

reconsider ll = il as Element of NAT by ORDINAL1:def 12;

reconsider il1 = ll as Element of Values (IC ) by MEMSTR_0:def 6;

set I = i;

set t = the State of S;

set P = the Instruction-Sequence of S;

assume A3: x = il + 1 ; :: thesis: x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il }

reconsider u = the State of S +* ((IC ),il1) as Element of product (the_Values_of S) by CARD_3:107;

ll in NAT ;

then A4: il in dom the Instruction-Sequence of S by PARTFUN1:def 2;

A5: ( the Instruction-Sequence of S +* (il,i)) /. ll = ( the Instruction-Sequence of S +* (il,i)) . ll by PBOOLE:143

.= i by A4, FUNCT_7:31 ;

IC in dom the State of S by MEMSTR_0:2;

then A6: IC u = il by FUNCT_7:31;

then IC (Following (( the Instruction-Sequence of S +* (il,i)),u)) = il + 1 by A1, A5;

hence x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } by A3, A6, A5; :: thesis: verum

end;reconsider il1 = ll as Element of Values (IC ) by MEMSTR_0:def 6;

set I = i;

set t = the State of S;

set P = the Instruction-Sequence of S;

assume A3: x = il + 1 ; :: thesis: x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il }

reconsider u = the State of S +* ((IC ),il1) as Element of product (the_Values_of S) by CARD_3:107;

ll in NAT ;

then A4: il in dom the Instruction-Sequence of S by PARTFUN1:def 2;

A5: ( the Instruction-Sequence of S +* (il,i)) /. ll = ( the Instruction-Sequence of S +* (il,i)) . ll by PBOOLE:143

.= i by A4, FUNCT_7:31 ;

IC in dom the State of S by MEMSTR_0:2;

then A6: IC u = il by FUNCT_7:31;

then IC (Following (( the Instruction-Sequence of S +* (il,i)),u)) = il + 1 by A1, A5;

hence x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } by A3, A6, A5; :: thesis: verum

now :: thesis: ( x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } implies x = il + 1 )

hence
( x in {(il + 1)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )
by A2, TARSKI:def 1; :: thesis: verumassume
x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il }
; :: thesis: x = il + 1

then ex s being Element of product (the_Values_of S) st

( x = IC (Exec (i,s)) & IC s = il ) ;

hence x = il + 1 by A1; :: thesis: verum

end;then ex s being Element of product (the_Values_of S) st

( x = IC (Exec (i,s)) & IC s = il ) ;

hence x = il + 1 by A1; :: thesis: verum