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 ;
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 ) ;
suppose InsCode i = 0 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 1 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 2 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 3 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 4 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 5 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
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 ;
hence UsedIntLoc (IncAddr (i,k)) = {} by Th15
.= UsedIntLoc i by ;
:: thesis: verum
end;
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 ;
hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16
.= UsedIntLoc i by ;
:: thesis: verum
end;
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 ;
hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16
.= UsedIntLoc i by ;
:: thesis: verum
end;
suppose InsCode i = 9 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 10 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 11 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
suppose InsCode i = 12 ; :: thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k))
end;
end;