let I be Program of ; :: thesis: UsedI*Loc I = UsedI*Loc (Directed I)

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

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

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

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

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

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

proof

{ (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } c= { (UsedInt*Loc 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 { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } or e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng (Directed I) } )

assume e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } ; :: thesis: e in { (UsedInt*Loc 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 = UsedInt*Loc 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 { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I } ; :: thesis: e in { (UsedInt*Loc 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 = UsedInt*Loc 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: UsedInt*Loc i = UsedInt*Loc jend;

hence
e in { (UsedInt*Loc 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: UsedInt*Loc i = UsedInt*Loc j

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

thus UsedInt*Loc i = {} by A7, Th32

.= UsedInt*Loc j by A8, Th32 ; :: thesis: verum

end;thus UsedInt*Loc i = {} by A7, Th32

.= UsedInt*Loc j by A8, Th32 ; :: thesis: verum

proof

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

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

then consider i being Instruction of SCM+FSA such that

A9: e = UsedInt*Loc i and

A10: i in rng (Directed I) ;

consider x being object such that

A11: x in dom (Directed I) and

A12: (Directed I) . x = i by A10, FUNCT_1:def 3;

set j = I . x;

A13: x in dom I by A11, FUNCT_4:99;

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

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

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

then consider i being Instruction of SCM+FSA such that

A9: e = UsedInt*Loc i and

A10: i in rng (Directed I) ;

consider x being object such that

A11: x in dom (Directed I) and

A12: (Directed I) . x = i by A10, FUNCT_1:def 3;

set j = I . x;

A13: x in dom I by A11, FUNCT_4:99;

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

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

now :: thesis: UsedInt*Loc i = UsedInt*Loc jend;

hence
e in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in rng I }
by A9, A14; :: thesis: verumper cases
( j = halt SCM+FSA or j <> halt SCM+FSA )
;

end;

suppose A15:
j = halt SCM+FSA
; :: thesis: UsedInt*Loc i = UsedInt*Loc j

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

hence UsedInt*Loc i = {} by Th32

.= UsedInt*Loc j by A15, Th32 ;

:: thesis: verum

end;hence UsedInt*Loc i = {} by Th32

.= UsedInt*Loc j by A15, Th32 ;

:: thesis: verum