let i be Instruction of SCM+FSA ; :: thesis: for k being Element of NAT holds UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)
let k be Element of NAT ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)
A1: InsCode i <= 11 + 1 by SCMFSA_2:35;
A2: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A3: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;

per cases ( 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 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A1, A2, A3, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then i = halt SCM+FSA by SCMFSA_2:122;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:8; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a, b being Int-Location st i = a := b by SCMFSA_2:54;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:9; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a, b being Int-Location st i = AddTo a,b by SCMFSA_2:55;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:10; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a, b being Int-Location st i = SubFrom a,b by SCMFSA_2:56;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:11; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a, b being Int-Location st i = MultBy a,b by SCMFSA_2:57;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:12; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a, b being Int-Location st i = Divide a,b by SCMFSA_2:58;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:13; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then consider l being Element of NAT such that
A4: i = goto l by SCMFSA_2:59;
IncAddr i,k = goto (l + k) by A4, SCMFSA_4:14;
hence UsedInt*Loc (IncAddr i,k) = {} by Th36
.= UsedInt*Loc i by A4, Th36 ;
:: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then consider l being Element of NAT , a being Int-Location such that
A5: i = a =0_goto l by SCMFSA_2:60;
IncAddr i,k = a =0_goto (l + k) by A5, SCMFSA_4:15;
hence UsedInt*Loc (IncAddr i,k) = {} by Th36
.= UsedInt*Loc i by A5, Th36 ;
:: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then consider l being Element of NAT , a being Int-Location such that
A6: i = a >0_goto l by SCMFSA_2:61;
IncAddr i,k = a >0_goto (l + k) by A6, SCMFSA_4:16;
hence UsedInt*Loc (IncAddr i,k) = {} by Th36
.= UsedInt*Loc i by A6, Th36 ;
:: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a, b being Int-Location ex f being FinSeq-Location st i = b := f,a by SCMFSA_2:62;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:17; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a, b being Int-Location ex f being FinSeq-Location st i = f,a := b by SCMFSA_2:63;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:18; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a being Int-Location ex f being FinSeq-Location st i = a :=len f by SCMFSA_2:64;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:19; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:65;
hence UsedInt*Loc i = UsedInt*Loc (IncAddr i,k) by SCMFSA_4:20; :: thesis: verum

end;

end;