let a, b be Int-Location ; :: thesis: for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA st ( i = halt SCM+FSA or i = a := b or i = AddTo a,b or i = SubFrom a,b or i = MultBy a,b or i = Divide a,b or i = goto l or i = a =0_goto l or i = a >0_goto l ) holds
UsedInt*Loc i = {}
let l be Instruction-Location of SCM+FSA ; :: thesis: for i being Instruction of SCM+FSA st ( i = halt SCM+FSA or i = a := b or i = AddTo a,b or i = SubFrom a,b or i = MultBy a,b or i = Divide a,b or i = goto l or i = a =0_goto l or i = a >0_goto l ) holds
UsedInt*Loc i = {}
let i be Instruction of SCM+FSA ; :: thesis: ( ( i = halt SCM+FSA or i = a := b or i = AddTo a,b or i = SubFrom a,b or i = MultBy a,b or i = Divide a,b or i = goto l or i = a =0_goto l or i = a >0_goto l ) implies UsedInt*Loc i = {} )
assume ( i = halt SCM+FSA or i = a := b or i = AddTo a,b or i = SubFrom a,b or i = MultBy a,b or i = Divide a,b or i = goto l or i = a =0_goto l or i = a >0_goto l ) ; :: thesis: UsedInt*Loc i = {}
then ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:124;
hence UsedInt*Loc i = {} by Def3; :: thesis: verum