let I be Program of ; :: thesis: UsedILoc I = UsedILoc (Directed I)

set A = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } ;

set B = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ;

A1: { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) }

set A = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } ;

set B = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ;

A1: { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) }

proof

{ (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } c= { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I }
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } or e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } )

assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } ; :: thesis: e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) }

then consider i being Instruction of SCM+FSA such that

A2: e = UsedIntLoc i and

A3: i in rng I ;

consider x being object such that

A4: x in dom I and

A5: I . x = i by A3, FUNCT_1:def 3;

set j = (Directed I) . x;

x in dom (Directed I) by A4, FUNCT_4:99;

then A6: (Directed I) . x in rng (Directed I) by FUNCT_1:3;

reconsider j = (Directed I) . x as Instruction of SCM+FSA by A6;

end;assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } ; :: thesis: e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) }

then consider i being Instruction of SCM+FSA such that

A2: e = UsedIntLoc i and

A3: i in rng I ;

consider x being object such that

A4: x in dom I and

A5: I . x = i by A3, FUNCT_1:def 3;

set j = (Directed I) . x;

x in dom (Directed I) by A4, FUNCT_4:99;

then A6: (Directed I) . x in rng (Directed I) by FUNCT_1:3;

reconsider j = (Directed I) . x as Instruction of SCM+FSA by A6;

now :: thesis: UsedIntLoc i = UsedIntLoc jend;

hence
e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) }
by A2, A6; :: thesis: verumper cases
( i = halt SCM+FSA or i <> halt SCM+FSA )
;

end;

suppose A7:
i = halt SCM+FSA
; :: thesis: UsedIntLoc i = UsedIntLoc j

then
j = goto (card I)
by A4, A5, FUNCT_4:106;

hence UsedIntLoc i = UsedIntLoc j by Th15, A7, Th13; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc j by Th15, A7, Th13; :: thesis: verum

proof

hence
UsedILoc I = UsedILoc (Directed I)
by A1, XBOOLE_0:def 10; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } or e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I } )

assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ; :: thesis: e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I }

then consider i being Instruction of SCM+FSA such that

A8: e = UsedIntLoc i and

A9: i in rng (Directed I) ;

consider x being object such that

A10: x in dom (Directed I) and

A11: (Directed I) . x = i by A9, FUNCT_1:def 3;

set j = I . x;

A12: x in dom I by A10, FUNCT_4:99;

then A13: I . x in rng I by FUNCT_1:3;

reconsider j = I . x as Instruction of SCM+FSA by A13;

end;assume e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } ; :: thesis: e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I }

then consider i being Instruction of SCM+FSA such that

A8: e = UsedIntLoc i and

A9: i in rng (Directed I) ;

consider x being object such that

A10: x in dom (Directed I) and

A11: (Directed I) . x = i by A9, FUNCT_1:def 3;

set j = I . x;

A12: x in dom I by A10, FUNCT_4:99;

then A13: I . x in rng I by FUNCT_1:3;

reconsider j = I . x as Instruction of SCM+FSA by A13;

now :: thesis: UsedIntLoc i = UsedIntLoc jend;

hence
e in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in rng I }
by A8, A13; :: thesis: verumper cases
( j = halt SCM+FSA or j <> halt SCM+FSA )
;

end;

suppose A14:
j = halt SCM+FSA
; :: thesis: UsedIntLoc i = UsedIntLoc j

then
i = goto (card I)
by A11, FUNCT_4:106, A12;

hence UsedIntLoc i = UsedIntLoc j by A14, Th13, Th15; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc j by A14, Th13, Th15; :: thesis: verum