let i be Instruction of SCMPDS; :: thesis: for l being Element of NAT st ( for s being State of SCMPDS st IC s = l holds

(Exec (i,s)) . (IC ) = (IC s) + 1 ) holds

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

let l be Element of NAT ; :: thesis: ( ( for s being State of SCMPDS st IC s = l holds

(Exec (i,s)) . (IC ) = (IC s) + 1 ) implies NIC (i,l) = {(l + 1)} )

reconsider I = i as Instruction of SCMPDS ;

reconsider n = l as Element of NAT ;

assume A1: for s being State of SCMPDS st IC s = l holds

(Exec (i,s)) . (IC ) = (IC s) + 1 ; :: thesis: NIC (i,l) = {(l + 1)}

reconsider t = the l -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;

A4: IC t = l by MEMSTR_0:def 11;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(l + 1)} or x in NIC (i,l) )

assume x in {(l + 1)} ; :: thesis: x in NIC (i,l)

then A5: x = l + 1 by TARSKI:def 1;

IC (Exec (I,t)) = l + 1 by A1, A4;

hence x in NIC (i,l) by A5, A4; :: thesis: verum

(Exec (i,s)) . (IC ) = (IC s) + 1 ) holds

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

let l be Element of NAT ; :: thesis: ( ( for s being State of SCMPDS st IC s = l holds

(Exec (i,s)) . (IC ) = (IC s) + 1 ) implies NIC (i,l) = {(l + 1)} )

reconsider I = i as Instruction of SCMPDS ;

reconsider n = l as Element of NAT ;

assume A1: for s being State of SCMPDS st IC s = l holds

(Exec (i,s)) . (IC ) = (IC s) + 1 ; :: thesis: NIC (i,l) = {(l + 1)}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(l + 1)} c= NIC (i,l)

set t = the l -started State of SCMPDS;let x be object ; :: thesis: ( x in NIC (i,l) implies x in {(l + 1)} )

assume x in NIC (i,l) ; :: thesis: x in {(l + 1)}

then consider s being Element of product (the_Values_of SCMPDS) such that

A2: x = IC (Exec (i,s)) and

A3: IC s = l ;

x = l + 1 by A1, A2, A3;

hence x in {(l + 1)} by TARSKI:def 1; :: thesis: verum

end;assume x in NIC (i,l) ; :: thesis: x in {(l + 1)}

then consider s being Element of product (the_Values_of SCMPDS) such that

A2: x = IC (Exec (i,s)) and

A3: IC s = l ;

x = l + 1 by A1, A2, A3;

hence x in {(l + 1)} by TARSKI:def 1; :: thesis: verum

reconsider t = the l -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;

A4: IC t = l by MEMSTR_0:def 11;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(l + 1)} or x in NIC (i,l) )

assume x in {(l + 1)} ; :: thesis: x in NIC (i,l)

then A5: x = l + 1 by TARSKI:def 1;

IC (Exec (I,t)) = l + 1 by A1, A4;

hence x in NIC (i,l) by A5, A4; :: thesis: verum