let i be Instruction of SCM+FSA; :: thesis: for k being Nat holds UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

let k be Nat; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

InsCode i <= 12 by SCMFSA_2:16;

then not not InsCode i = 0 & ... & not InsCode i = 12 ;

let k be Nat; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

InsCode i <= 12 by SCMFSA_2:16;

then not not InsCode i = 0 & ... & not InsCode i = 12 ;

per cases 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 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 )
;

end;

suppose
InsCode i = 0
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
i = halt SCM+FSA
by SCMFSA_2:95;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 1
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a, b being Int-Location st i = a := b
by SCMFSA_2:30;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 2
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a, b being Int-Location st i = AddTo (a,b)
by SCMFSA_2:31;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 3
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a, b being Int-Location st i = SubFrom (a,b)
by SCMFSA_2:32;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 4
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a, b being Int-Location st i = MultBy (a,b)
by SCMFSA_2:33;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 5
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a, b being Int-Location st i = Divide (a,b)
by SCMFSA_2:34;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 6
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then consider l being Nat such that

A1: i = goto l by SCMFSA_2:35;

IncAddr (i,k) = goto (l + k) by A1, SCMFSA_4:1;

hence UsedIntLoc (IncAddr (i,k)) = {} by Th15

.= UsedIntLoc i by A1, Th15 ;

:: thesis: verum

end;A1: i = goto l by SCMFSA_2:35;

IncAddr (i,k) = goto (l + k) by A1, SCMFSA_4:1;

hence UsedIntLoc (IncAddr (i,k)) = {} by Th15

.= UsedIntLoc i by A1, Th15 ;

:: thesis: verum

suppose
InsCode i = 7
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then consider l being Nat, a being Int-Location such that

A2: i = a =0_goto l by SCMFSA_2:36;

IncAddr (i,k) = a =0_goto (l + k) by A2, SCMFSA_4:2;

hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16

.= UsedIntLoc i by A2, Th16 ;

:: thesis: verum

end;A2: i = a =0_goto l by SCMFSA_2:36;

IncAddr (i,k) = a =0_goto (l + k) by A2, SCMFSA_4:2;

hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16

.= UsedIntLoc i by A2, Th16 ;

:: thesis: verum

suppose
InsCode i = 8
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then consider l being Nat, a being Int-Location such that

A3: i = a >0_goto l by SCMFSA_2:37;

IncAddr (i,k) = a >0_goto (l + k) by A3, SCMFSA_4:3;

hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16

.= UsedIntLoc i by A3, Th16 ;

:: thesis: verum

end;A3: i = a >0_goto l by SCMFSA_2:37;

IncAddr (i,k) = a >0_goto (l + k) by A3, SCMFSA_4:3;

hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16

.= UsedIntLoc i by A3, Th16 ;

:: thesis: verum

suppose
InsCode i = 9
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a)
by SCMFSA_2:38;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 10
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b
by SCMFSA_2:39;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 11
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a being Int-Location ex f being FinSeq-Location st i = a :=len f
by SCMFSA_2:40;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

suppose
InsCode i = 12
; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

then
ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a
by SCMFSA_2:41;

hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum

end;hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; :: thesis: verum