let p be preProgram of SCM+FSA; for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for a, b being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedILoc p & b in UsedILoc p )
let ic be Instruction of SCM+FSA; for fa being FinSeq-Location
for a, b being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedILoc p & b in UsedILoc p )
let fa be FinSeq-Location ; for a, b being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedILoc p & b in UsedILoc p )
let a, b be Int-Location; ( ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) implies ( a in UsedILoc p & b in UsedILoc p ) )
assume that
A1:
ic in rng p
and
A2:
( ic = b := (fa,a) or ic = (fa,a) := b )
; ( a in UsedILoc p & b in UsedILoc p )
A3:
UsedIntLoc ic = {a,b}
by A2, SF_MASTR:17;
UsedIntLoc ic c= UsedILoc p
by A1, SF_MASTR:19;
hence
( a in UsedILoc p & b in UsedILoc p )
by A3, ZFMISC_1:32; verum