let a, b be Int-Location; :: thesis: for i being Instruction of SCM+FSA st ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) holds
UsedIntLoc i = {a,b}
let i be Instruction of SCM+FSA; :: thesis: ( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) implies UsedIntLoc i = {a,b} )
reconsider ab = {a,b} as Element of Fin Int-Locations by FINSUB_1:def 5;
assume A1: ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) ; :: thesis: UsedIntLoc i = {a,b}
then not not InsCode i = 1 & ... & not InsCode i = 5 by SCMFSA_2:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22;
then InsCode i in {1,2,3,4,5} by ENUMSET1:def 3;
then UsedIntLoc i = ab by A1, Def1;
hence UsedIntLoc i = {a,b} ; :: thesis: verum