let a, b be Int-Location; :: thesis: for l being 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 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 not not InsCode i = 0 & ... & not InsCode i = 8 by COMPOS_1:70, SCMFSA_2:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25;
hence UsedInt*Loc i = {} by Def4; :: thesis: verum