In mmb.md, the description of the Thm opcode's behavior includes this:
* For each argument `ei`:
* check that `sort(ei) = thm[T].args[i].sort`
* If `thm[T].args[i].bound`:
* check that `bound(ei)`.
* check that `FV(e') ∩ FV(ei) = {}` for all `e'` in `uheap`
* push `FV(ei)` to `deps`
* Otherwise:
* For each `j` such that `thm[T].args[i].deps[j]`:
* check that `deps[j] ∩ FV(ei) = {}`
* Push `ei` to `uheap`
But I'm having a little trouble reconciling this with the paper and with mm0-c.
- Should
FV here be V, since theorem admissibility seems to use V rather than FV?
- In the
Otherwise clause, is the condition reversed? My understanding from mm0-c is that for each earlier bound variable index j, the check is that either thm[T].args[i].deps[j] is set, or else the recorded earlier bound variable substitution deps[j] is disjoint from V(ei). In other words, something like: thm[T].args[i].deps[j] || deps[j] ∩ V(ei) = {}
I may be misunderstanding the intended reading here, so I'd be grateful for clarification either way.
In mmb.md, the description of the
Thmopcode's behavior includes this:But I'm having a little trouble reconciling this with the paper and with
mm0-c.FVhere beV, since theorem admissibility seems to useVrather thanFV?Otherwiseclause, is the condition reversed? My understanding frommm0-cis that for each earlier bound variable indexj, the check is that eitherthm[T].args[i].deps[j]is set, or else the recorded earlier bound variable substitutiondeps[j]is disjoint fromV(ei). In other words, something like:thm[T].args[i].deps[j] || deps[j] ∩ V(ei) = {}I may be misunderstanding the intended reading here, so I'd be grateful for clarification either way.