41 lines
No EOL
1.5 KiB
Text
41 lines
No EOL
1.5 KiB
Text
#import "@preview/prooftrees:0.1.0": *
|
|
|
|
#let natrec = text[natrec]
|
|
#let suc = text[suc]
|
|
|
|
= Problem 1
|
|
|
|
Define `funsplit` in terms of `apply`.
|
|
|
|
$ "funsplit"(f, d) &equiv d("apply"(f, (x) x)) $
|
|
|
|
In the case of $f = lambda b$ the following evaluation occurs:
|
|
|
|
$ "funsplit"(lambda b, d) &equiv d( "apply"(lambda b, (x) x)) \
|
|
&equiv d(((x)x)(b)) \
|
|
&equiv d(b) $
|
|
|
|
= Problem 2
|
|
|
|
Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:
|
|
|
|
$ plus.circle(x, 0) = x ∈ NN [x ∈ NN] $
|
|
|
|
Please be pedantic and explicitly use a rule even for "obvious" steps. You do not have to draw a big derivation tree (which is difficult to typeset), but it should be clear which rule you are using at each step. If you are using an implicit rule that the authors did not explicitly write out, make it clear what it is. If you are not sure what a derivation tree is, whether a particular rule is allowed, or which emoji was just introduced in Emoji 15.1, use the Discord forum immediately.
|
|
|
|
#{
|
|
tree(
|
|
axi[$C(v) "set" [v in NN]$],
|
|
axi[$x in NN$],
|
|
axi[$d in C(0)$],
|
|
axi[$x in NN$],
|
|
nary(4)[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],
|
|
)
|
|
|
|
tree(
|
|
axi[],
|
|
uni[$plus.circle(x, 0) equiv natrec(x, 0, (u, v) suc(v)) [Gamma tack.r x in NN]$],
|
|
axi[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],
|
|
bin[$plus.circle(x, 0) equiv x in NN [(Gamma, Delta) tack.r x in NN]$],
|
|
)
|
|
} |