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} )
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}
( a in Int-Locations & b in Int-Locations ) by SCMFSA_2:9;
then {a,b} c= Int-Locations by ZFMISC_1:38;
then reconsider ab = {a,b} as Element of Fin Int-Locations by FINSUB_1:def 5;
( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) by A1, SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46;
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