let l be Element of NAT ; :: thesis: for k being Integer holds NIC ((goto k),l) = {|.(k + l).|}
let k be Integer; :: thesis: NIC ((goto k),l) = {|.(k + l).|}
set s = the State of SCMPDS;
set i = goto k;
set t = |.(k + l).|;
set I = goto k;
reconsider n = l as Element of NAT ;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {|.(k + l).|} c= NIC ((goto k),l)
let x be object ; :: thesis: ( x in NIC ((goto k),l) implies x in {|.(k + l).|} )
assume x in NIC ((goto k),l) ; :: thesis: x in {|.(k + l).|}
then consider s being Element of product (the_Values_of SCMPDS) such that
A1: x = IC (Exec ((goto k),s)) and
A2: IC s = l ;
A3: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst (s,k) = |.(m1 + k).| ) by SCMPDS_2:def 18;
x = |.(k + l).| by A1, A2, A3, SCMPDS_2:54;
hence x in {|.(k + l).|} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {|.(k + l).|} or x in NIC ((goto k),l) )
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A4: IC u = n by MEMSTR_0:def 11;
consider m1 being Element of NAT such that
A5: m1 = IC u and
A6: ICplusConst (u,k) = |.(m1 + k).| by SCMPDS_2:def 18;
assume x in {|.(k + l).|} ; :: thesis: x in NIC ((goto k),l)
then x = |.(m1 + k).| by A4, A5, TARSKI:def 1
.= IC (Exec ((goto k),u)) by A6, SCMPDS_2:54 ;
hence x in NIC ((goto k),l) by A4; :: thesis: verum