Obelisk semantics

I'm just a chuftie, been working on the semantics. Trying to be precise without being too verbose in my logic.

I want to share some, because I'm just happy that the snm math plugin is working well.

In English:

A function definition F only has correct scoping when the set of its where clause constants Wc have correct scoping and the set of its where clause function definitions Wf have correct scopping and its block Fb has correct scoping.

The source (I use '.' to separate constraints for readability):

forsome F.
Fb member F. Fb = Block.
Wc member F. Wc = Set. forall C. C member Wc. C = ConstantDefinition.
Wf member F. Wf = Set. forall G. G member Wf. G = FunctionDefinition.
forsome S. forsome Bq. forsome Wcq. forsome Wfq.
new_scope(Fb, S, Bq). new_scope(Wc, S, Wcq). new_scope(Wf, S, Wfq).
scope(F, S) iff scope(Fb, Bq) and scope(Wc, Wcq) and scope(Wf, Wfq)

Output:

∃ F.
Fb ∈ F. Fb = Block.
Wc ∈ F. Wc = Set. ∀ C. C ∈ Wc. C = ConstantDefinition.
Wf ∈ F. Wf = Set. ∀ G. G ∈ Wf. G = FunctionDefinition.
∃ S. ∃ Bq. ∃ Wcq. ∃ Wfq.
new_scope(Fb, S, Bq). new_scope(Wc, S, Wcq). new_scope(Wf, S, Wfq).
scope(F, S) ⇔ scope(Fb, Bq) ∧ scope(Wc, Wcq) ∧ scope(Wf, Wfq)

Probably doesn't make any sense as I haven't declared what the new_scopes are for the block, where clause elements etc, but I think it looks pretty cool.