let R be Ring; :: thesis: for il, i1 being Nat holds NIC ((goto (i1,R)),il) = {i1}

let il, i1 be Nat; :: thesis: NIC ((goto (i1,R)),il) = {i1}

let il, i1 be Nat; :: thesis: NIC ((goto (i1,R)),il) = {i1}

now :: thesis: for x being object holds

( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )

hence
NIC ((goto (i1,R)),il) = {i1}
by TARSKI:2; :: thesis: verum( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )

let x be object ; :: thesis: ( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )

A1: il in NAT by ORDINAL1:def 12;

end;A1: il in NAT by ORDINAL1:def 12;

A2: now :: thesis: ( x = i1 implies x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )

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

set I = goto (i1,R);

set t = the State of (SCM R);

set Q = the Instruction-Sequence of (SCM R);

assume A3: x = i1 ; :: thesis: x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il }

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

reconsider P = the Instruction-Sequence of (SCM R) +* (il,(goto (i1,R))) as Instruction-Sequence of (SCM R) ;

A4: P /. il = P . il by PBOOLE:143, A1;

IC in dom the State of (SCM R) by MEMSTR_0:2;

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

il in NAT by ORDINAL1:def 12;

then il in dom the Instruction-Sequence of (SCM R) by PARTFUN1:def 2;

then A6: P . il = goto (i1,R) by FUNCT_7:31;

then IC (Following (P,u)) = i1 by A5, A4, SCMRING2:15;

hence x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } by A3, A4, A5, A6; :: thesis: verum

end;set I = goto (i1,R);

set t = the State of (SCM R);

set Q = the Instruction-Sequence of (SCM R);

assume A3: x = i1 ; :: thesis: x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il }

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

reconsider P = the Instruction-Sequence of (SCM R) +* (il,(goto (i1,R))) as Instruction-Sequence of (SCM R) ;

A4: P /. il = P . il by PBOOLE:143, A1;

IC in dom the State of (SCM R) by MEMSTR_0:2;

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

il in NAT by ORDINAL1:def 12;

then il in dom the Instruction-Sequence of (SCM R) by PARTFUN1:def 2;

then A6: P . il = goto (i1,R) by FUNCT_7:31;

then IC (Following (P,u)) = i1 by A5, A4, SCMRING2:15;

hence x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } by A3, A4, A5, A6; :: thesis: verum

now :: thesis: ( x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } implies x = i1 )

hence
( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )
by A2, TARSKI:def 1; :: thesis: verumassume
x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il }
; :: thesis: x = i1

then ex s being Element of product (the_Values_of (SCM R)) st

( x = IC (Exec ((goto (i1,R)),s)) & IC s = il ) ;

hence x = i1 by SCMRING2:15; :: thesis: verum

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

( x = IC (Exec ((goto (i1,R)),s)) & IC s = il ) ;

hence x = i1 by SCMRING2:15; :: thesis: verum