let a, b be Int-Location ; :: thesis: for l being Element of NAT
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 Element of NAT ; :: 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:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25, SCMFSA_2:97;
hence UsedInt*Loc i = {} by Def3; :: thesis: verum