# A Game Theoretic Framework for Surplus Food Distribution in Smart Cities and Beyond
## 2 Materials and Methods
### Proposed Mechanism
#### 2.2.2 The NUIR Sub-Process
: We prove this using the loop invariant technique [64]. We start our proof with the main FDRM-CA algorithm and then we detail the inner sub-processes. **Algorithm 1 (The FDRM-CA Mechanism):** here, we use the following loop invariant:  
At the start of the \(i\)th iteration of the for loop of lines 5-13, each receiver \(\mathbb{R}_{j}\) processed in the prior \((i-1)\) iterations have their best available donors allocated, respecting the eligible donors' preference lists. **Initialization:** prior to the first iteration of the loop, \(i=1\), there are no receivers processed and no matching exists. This trivially satisfies the invariant. **Maintenance:** At any iteration \(i\) of the loop, each receiver \(\mathbb{R}_{j}\) processed is classified into either _perishable_ or _non-perishable_ category. Thereafter, for each donor in the priority list of \(\mathbb{R}_{j}\), the donor's ranking of \(\mathbb{R}_{j}\) is retrieved. The donor \(\mathbb{D}_{k}\) with the highest ranking for \(\mathbb{R}_{j}\) is assigned to \(\mathbb{R}_{j}\). Furthermore, \(i\) is used for the next iteration of the **for** loop maintains the invariant. Of course, the correctness of the above step depends on the correctness of the inner sub-parts, which is proven later in this section. **Termination:** At termination, when \(i=n+1\), each receiver \(\mathbb{R}_{j}\) processed in the prior \(n\) iterations has the best available donors allocated, respecting the eligible donors' preference lists. This proves that the FDRM-CA algorithm works correctly. To reinforce the maintenance step of this proof, following are the additional proofs of correctness of the sub-processes of this algorithm. **Algorithm 2 (The NUIR Sub-Process):** This can be proved along similar lines as above and is included in Appendix A. **Algorithm 3 (The CTFU Sub-Process):** Here, we use the following loop invariant:  
At the start of the \(i\)th iteration of the foreach loop of lines 1-13, the first \((i-1)\) agent requests from \(\mathbb{C}\), processed in the prior \((i-1)\) iterations, have been classified and appended to one of the five lists, namely, \(\mathbb{V}\), \(\mathbb{PFD}\), \(\mathbb{NPFD}\), \(\mathbb{PFR}\), \(\mathbb{NPFR}\). **Initialization:** Prior to the first iteration of the foreach loop, there are no agent requests processed, and this trivially satisfies the invariant. **Maintenance:** In the \(i\)th iteration, the \(i\)th agent request is taken up for processing from the list \(\mathbb{C}\). If this agent request is a volunteer request, it is appended to the list \(\mathbb{V}\). If not, it is classified and appended to one of the four food request lists, namely, \(\mathbb{PFD}\), \(\mathbb{NPFD}\), \(\mathbb{PFR}\), and \(\mathbb{NPFR}\). Observe that, prior to this iteration, all the five lists, namely, \(\mathbb{V}\), \(\mathbb{PFD}\), \(\mathbb{NPFD}\), \(\mathbb{PFR}\), \(\mathbb{NPFR}\), already had a total of \((i-1)\) agent requests from \(\mathbb{C}\) classified and appended to them from the \((i-1)\) prior iterations. As the foreach loop picks up the next agent request from \(\mathbb{C}\) for the next iteration, the loop invariant is re-established. **Termination:** At termination, the list \(\mathbb{C}\) is empty and all agent requests have been classified and appended to one of the five lists, namely, \(\mathbb{V}\), \(\mathbb{PFD}\), \(\mathbb{NPFD}\), \(\mathbb{PFR}\), \(\mathbb{NPFR}\). Thus, the invariant is maintained. This proves that the CTFU process works correctly. **Algorithm 4 (The CA-DTB Sub-Process):** This can be proved along similar lines as above and is included in Appendix A. By having proven the correctness of all its sub-parts, this concludes our proof of correctness of the FDRM-CA mechanism.