pantagruel

remove_groups report: Report.
" An expense report consists of an ordered series of reimbursement requests,
" each of which has a requester, a memo, and and amount.
Report <= [Request].
req (requester, memo):String, amount: Nat => Request.
---
all r: report ..
    (r.requester in group_table ->
        ~(r in report')
        and
        all group_member:(group_table r.requester) ..
            (req group_member r.memo (r.amount % #(group_table r.requester))) in report'
    )
    and (~(r.requester in group_table) -> r in report').

;
" Groups are tracked in a table which relates a group name to the names
" of its members.
group_table requester_name: String :: {String}.