let a be Data-Location; :: thesis: for il, k being Nat holds NIC ((a =0_goto k),il) = {k,(il + 1)}
let il, k be Nat; :: thesis: NIC ((a =0_goto k),il) = {k,(il + 1)}
set t = the State of SCM;
set Q = the Instruction-Sequence of SCM;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {k,(il + 1)} c= NIC ((a =0_goto k),il)
let x be object ; :: thesis: ( x in NIC ((a =0_goto k),il) implies b1 in {k,(il + 1)} )
assume x in NIC ((a =0_goto k),il) ; :: thesis: b1 in {k,(il + 1)}
then consider s being Element of product such that
A1: ( x = IC (Exec ((a =0_goto k),s)) & IC s = il ) ;
per cases ( s . a = 0 or s . a <> 0 ) ;
suppose s . a = 0 ; :: thesis: b1 in {k,(il + 1)}
then x = k by ;
hence x in {k,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
suppose s . a <> 0 ; :: thesis: b1 in {k,(il + 1)}
then x = il + 1 by ;
hence x in {k,(il + 1)} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {k,(il + 1)} or x in NIC ((a =0_goto k),il) )
set I = a =0_goto k;
A2: IC <> a by AMI_5:2;
reconsider n = il as Element of NAT by ORDINAL1:def 12;
reconsider il1 = n as Element of Values () by MEMSTR_0:def 6;
reconsider u = the State of SCM +* ((),il1) as Element of product by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM +* (il,(a =0_goto k)) as Instruction-Sequence of SCM ;
assume A3: x in {k,(il + 1)} ; :: thesis: x in NIC ((a =0_goto k),il)
per cases ( x = k or x = il + 1 ) by ;
suppose A4: x = k ; :: thesis: x in NIC ((a =0_goto k),il)
reconsider v = u +* () as Element of product by CARD_3:107;
A5: IC in dom the State of SCM by MEMSTR_0:2;
not IC in dom () by ;
then A7: IC v = IC u by FUNCT_4:11
.= n by ;
reconsider il = il as Element of NAT by ORDINAL1:def 12;
A8: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;
then A9: P . il = a =0_goto k by FUNCT_7:31;
a in dom () by TARSKI:def 1;
then v . a = () . a by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
then IC (Following (P,v)) = k by ;
hence x in NIC ((a =0_goto k),il) by A4, A7, A9, A8; :: thesis: verum
end;
suppose A10: x = il + 1 ; :: thesis: x in NIC ((a =0_goto k),il)
reconsider v = u +* (a .--> 1) as Element of product by CARD_3:107;
A11: IC in dom the State of SCM by MEMSTR_0:2;
not IC in dom (a .--> 1) by ;
then A13: IC v = IC u by FUNCT_4:11
.= n by ;
reconsider il = il as Element of NAT by ORDINAL1:def 12;
A14: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;
then A15: P . il = a =0_goto k by FUNCT_7:31;
a in dom (a .--> 1) by TARSKI:def 1;
then v . a = (a .--> 1) . a by FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
then IC (Following (P,v)) = il + 1 by ;
hence x in NIC ((a =0_goto k),il) by A10, A13, A15, A14; :: thesis: verum
end;
end;