\defded{td-treeA}{ \infer{ ° z }{ \infer{ ° y }{ x\land y } & \infer{ ° y\to z }{ \infer{ ° x }{ x\land y } & x\to (y\to z) } } } \defded{td-dbar}{ \infer={ ° z }{ \infer={ ° x\land y }{ V } & \infer={ ° x\to (y\to z) }{ W } } } \defded{td-TA}{ \infer[\ruleT\DN\treeA]{ ° z }{ \infer={ ° x\land y }{ V } & \infer={ ° x\to (y\to z) }{ W } } } \defded{td-TeA}{ \infer[1:\ruleTe\DN]{ ° z }{ \infer={ ° x\land y }{ V } & \infer={ ° x\to (y\to z) }{ W } & \infer{ ° z }{ \infer{ ° y }{ [x\land y]^{1A} } & \infer{ ° y\to z }{ \infer{ ° x }{ [x\land y]^{1A} } & [x\to (y\to z)]^{1B} } } } } \defded{td-Adireto}{ \infer{ ° z }{ \infer{ ° y }{ \infer={ ° x\land y }{ V } } & \infer{ ° y\to z }{ \infer{ ° x }{ \infer={ ° x\land y }{ V } } & \infer={ ° x\to (y\to z) }{ W } } } } \defded{td-CCCcur}{ \infer[\cur]{ ° {\alpha}\to ({\beta}\to {\gamma}) }{ {\alpha}\land {\beta}\to {\gamma} } } \defded{td-DNcur}{ \infer[3:\ruleTe\DN]{ ° {\alpha}\to ({\beta}\to {\gamma}) }{ {\alpha}\land {\beta}\to {\gamma} & \infer[2]{ ° {\alpha}\to ({\beta}\to {\gamma}) }{ \infer[1]{ ° {\beta}\to {\gamma} }{ \infer{ ° c }{ \infer{ ° {\alpha}\land {\beta} }{ [{\alpha}]^2 & [{\beta}]^1 } & [{\alpha}\land {\beta}\to {\gamma}]^{3A} } } } } } \defded{DN->CCC.1}{ \infer{ ° b\land a }{ \infer{ ° b }{ a\land b } & \infer{ ° a }{ a\land b } } } \defded{DN->CCC.2}{ \infer[\ruleTCCC]{ ° õ\to b\land a }{ \infer[\ruleTCCC]{ ° õ\to b }{ õ\to a\land b } & \infer[\ruleTCCC]{ ° õ\to a }{ õ\to a\land b } } } \defded{tdex1}{ \infer[2]{ ° abc\to ac }{ \infer[1]{ ° ac }{ \infer{ ° c }{ \infer{ ° b }{ [a]^1 & \infer{ ° ab }{ [abc]^2 } } & \infer{ ° bc }{ [abc]^2 } } } } } \defded{tdex2}{ \infer[2]{ ° õ\TO abc\to ac }{ \infer[1]{ ° abc_2\TO ac }{ \infer{ ° a_1\LAND abc_2\TO c }{ \infer{ ° a_1\LAND abc_2\TO b }{ \infer{ ° a_1\TO a }{} & \infer{ ° abc_2\TO ab }{ \infer{ ° abc_2\TO abc }{} } } & \infer{ ° abc_2\TO bc }{ \infer{ ° abc_2\TO abc }{} } } } } } \defded{tdnum-1}{ \infer{ ° a_1\LAND a_2\LAND a_3\TO c }{ a_1\LAND a_2\TO b & a_2\LAND a_3\TO b\to c } } \defded{tdnum-2}{ \infer{ ° a_1\LAND a_2\LAND a_3\TO c }{ a_1\LAND a_2\LAND a_3\TO b & a_1\LAND a_2\LAND a_3\TO b\to c } } \defded{tdnum-3}{ \infer{ ° õ\to b }{ \infer{ ° õ\to (b\land (b\to c)) }{ õ\to b & õ\to (b\to c) } & \infer{ ° b\land (b\to c)\ton{\ev}c }{} } } \defded{tdex-step}{ \infer{ ° a1\land abc2\to c }{ \infer{ ° a1\land abc2\to b\land bc }{ a1\land abc2\to b & \infer{ ° a1\land abc2\to bc }{ \infer{ ° a1\land abc2\to abc2 }{} & abc2\to bc } } & \infer{ ° b\land bc\to c }{} } } \defded{a->a}{ \infer[1]{ ° {\alpha}\to {\alpha} }{ [{\alpha}]^1 } } \defded{a->c}{ \infer[1]{ ° {\alpha}\to {\gamma} }{ \infer{ ° {\gamma} }{ \infer{ ° {\beta} }{ [{\alpha}]^1 & {\alpha}\to {\beta} } & {\beta}\to {\gamma} } } } \defded{a->T}{ \infer[1]{ ° {\alpha}\to õ }{ \infer{ ° õ }{} } } \defded{T->a}{ \infer[1]{ ° õ\to {\alpha} }{ {\alpha} } } \defded{T->a=>a}{ \infer{ ° {\alpha} }{ \infer{ ° õ }{} & õ\to {\alpha} } } \defded{a1vb1->a2vb2}{ \infer[2]{ ° {\alpha}_1\lor {\beta}_1\to {\alpha}_2\lor {\beta}_2 }{ \infer[1]{ ° {\alpha}_2\lor {\beta}_2 }{ [{\alpha}_1\lor {\beta}_1]^2 & \infer{ ° {\alpha}_2\lor {\beta}_2 }{ \infer{ ° {\alpha}_2 }{ [{\alpha}_1]^1 & {\alpha}_1\to {\alpha}_2 } } & \infer{ ° {\alpha}_2\lor {\beta}_2 }{ \infer{ ° {\beta}_2 }{ [{\beta}_1]^1 & {\beta}_1\to {\beta}_2 } } } } } \defded{a<=T}{ \infer[1]{ ° {\alpha}\to õ }{ \infer{ ° õ }{} } } \defded{0<=a}{ \infer[1]{ ° ©\to {\alpha} }{ \infer{ ° {\alpha} }{ [©]^1 } } } \defded{hey-andE}{ \infer[1]{ ° {\alpha}\to b/c }{ \infer{ ° b/c }{ \infer{ ° b\land c }{ [{\alpha}]^1 & {\alpha}\to b\land c } } } } \defded{hey-andI}{ \infer[1]{ ° {\alpha}\to {\beta}\land {\gamma} }{ \infer{ ° {\beta}\land {\gamma} }{ \infer{ ° {\beta} }{ [{\alpha}]^1 & {\alpha}\to {\beta} } & \infer{ ° {\gamma} }{ [{\alpha}]^1 & {\alpha}\to {\gamma} } } } } \defded{hey-orE}{ \infer[1]{ ° b\to d }{ \infer{ ° d }{ \infer{ ° b\lor c }{ [b]^1 } & b\lor c\to d } } } \defded{hey-orI}{ \infer[2]{ ° b\lor c\to d }{ \infer[1]{ ° d }{ [b\lor c]^2 & \infer{ ° d }{ [b]^1 & b\to d } & \infer{ ° d }{ [c]^1 & c\to d } } } } \defded{hey-uncur}{ \infer[1]{ ° {\alpha}\land b\to c }{ \infer{ ° c }{ \infer{ ° b }{ [{\alpha}\land b]^1 } & \infer{ ° b\to c }{ \infer{ ° {\alpha} }{ [{\alpha}\land b]^1 } & {\alpha}\to (b\to c) } } } } \defded{hey-cur}{ \infer[2]{ ° {\alpha}\to (b\to c) }{ \infer[1]{ ° b\to c }{ \infer{ ° c }{ \infer{ ° {\alpha}\land b }{ [{\alpha}]^2 & [b]^1 } & {\alpha}\land b\to c } } } } \defded{Heyting1}{ \infer{ ° b\land a }{ \infer{ ° b }{ [a\land b]^1 } & \infer{ ° a }{ [a\land b]^1 } } } \defded{Heyting2}{ \infer{ ° a\land b\to b\to a }{ \infer{ ° a\land b\to b }{} & \infer{ ° a\land b\to a }{} } } \defded{AvnA}{ \infer{ ° A\lor ªA }{ A & \infer{ ° ªA }{ A } } } \defded{AvnA.w3}{ \infer{ ° \cpoV 101 }{ \cpoV 100 & \infer{ ° \cpoV 001 }{ \cpoV 100 } } } \defded{B->nnB}{ \infer{ ° B\to ªªB }{ B & \infer{ ° ªªB }{ \infer{ ° ªB }{ B } } } } \defded{B->nnB.w2}{ \infer{ ° \cpoDois 01 }{ \cpoDois 01 & \infer{ ° \cpoDois 11 }{ \infer{ ° \cpoDois 00 }{ \cpoDois 01 } } } } \defded{demorgan}{ \infer{ ° ª(C\land D)\to (ªC\lor ªD) }{ \infer{ ° ª(C\land D) }{ \infer{ ° C\land D }{ C & D } } & \infer{ ° ªC\lor ªD }{ \infer{ ° ªC }{ C } & \infer{ ° ªD }{ D } } } } \defded{demorgan.w3}{ \infer{ ° \cpoV 101 }{ \infer{ ° \cpoV 111 }{ \infer{ ° \cpoV 000 }{ \cpoV 100 & \cpoV 001 } } & \infer{ ° \cpoV 101 }{ \infer{ ° \cpoV 001 }{ \cpoV 100 } & \infer{ ° \cpoV 100 }{ \cpoV 001 } } } } \defded{transf-1}{ \infer[\ruleF{(+)}]{ ° c }{ a & b } } \defded{transf-2}{ \infer[\ruleF{\ii\to (+)}]{ ° \ii\to c }{ \ii\to a & \ii\to b } } \defded{transf-3}{ \infer[\ruleF{\nss{(+)}}]{ ° \ns{c} }{ \ns{a} & \ns{b} } } \defded{transf-4}{ \infer[1]{ ° \ii\to c }{ \infer[\ruleF{(+)}]{ ° c }{ \infer{ ° a }{ [\ii]^1 & \ii\to a } & \infer{ ° b }{ [\ii]^1 & \ii\to b } } } } \defded{transfapp-1}{ \infer[\ruleF{\app}]{ ° f(a_1,\ldots,a_n) }{ a_1 & \ldots & a_n & f } } \defded{transfapp-2}{ \infer[\ruleF{\ii\to \app}]{ ° \ii\to f(a_1,\ldots,a_n) }{ \ii\to a_1 & \ldots & \ii\to a_n & \ii\to f } } \defded{transfapp-3}{ \infer[\ruleF{\nss{\app}}]{ ° \ns{f}(\ns{a_1},\ldots,\ns{a_n}) }{ \ns{a_1} & \ldots & \ns{a_n} & \ns{f} } } \defded{transfex-1}{ \infer{ ° P(x)\land ªQ(x,f(y)) }{ \infer{ ° P(x) }{ x & P } & \infer{ ° ªQ(x,f(y)) }{ \infer{ ° Q(x,f(y)) }{ x & \infer{ ° f(y) }{ y & f } & Q } & \t\ton{ª}\t } & \t,\t\ton{\land }\t } } \defded{transfex-2}{ \infer[1]{ ° Ðx.(P(x)\land ªQ(x,f(y))) }{ \infer{ ° P(x)\land ªQ(x,f(y)) }{ \infer{ ° P(x) }{ [x]^1 & P } & \infer{ ° ªQ(x,f(y)) }{ \infer{ ° Q(x,f(y)) }{ [x]^1 & \infer{ ° f(y) }{ y & f } & Q } & \t\ton{ª}\t } & \t,\t\ton{\land }\t } } } \defded{tfi1}{ \infer[\TFI]{ ° y\to x }{ x & x\to y & \ldots } } \defded{tfi-tflsub}{ \infer={ ° x\to y }{ \infer[\TFI]{ ° x\to t }{ t & \infer={ ° t\to x }{ t\to x\land y } } & t\to x\land y } } \defded{tfi-tfimp}{ \infer={ ° x\to y }{ \infer{ ° f }{ x\land y & x\land y\to f } & \infer={ ° x\land f\to y }{ \infer[\TFI]{ ° x\land f\to x\land y }{ x\land y & \infer={ ° x\land y\to x\land f }{ x\land y\to f } } } } } \defded{linear1}{ \infer[1]{ ° a\to c }{ \infer{ ° c }{ \infer{ ° b }{ [a]^1 & a\to b } & \infer{ ° b\to c }{ [a]^1 & a\to (b\to c) } } } } \defded{linear2}{ \infer[1]{ ° x\mapsto6x^2? }{ \infer{ ° 6x^2 }{ \infer{ ° 2x }{ [x]^1 & 2 } & \infer{ ° 3x }{ [x]^1 & 3 } } } } \defded{lineardx1}{ \infer{ ° dy }{ \infer{ ° !dx }{ dx } & !dx÷dy } } \defded{lineardx2}{ \infer{ ° dy=y_x{}dx+\frac{y_{xx}}{2}dx^2+\ldots }{ \infer{ ° (dx,dx^2,\ldots) }{ dx } & (y_x,\frac{y_{xx}}{2},\ldots) } } \defded{lineare1}{ \infer{ ° a\to b\land c }{ a\to b & a\to c } } \defded{lineare2}{ \infer{ ° a\land b\to c }{ a\to (b\to c) } } \defded{lineare3}{ \infer{ ° a÷(b¾c) }{ a÷b & a÷c } } \defded{lineare4}{ \infer{ ° (aÏb)÷c }{ a÷(b÷c) } } \defded{param-anddef}{ \infer[\eta]{ ° (a\land b)^P }{ \infer[1]{ ° (a\land b)^2\to a^{P2}\land b^{P2} }{ \infer{ ° a^{P2}\land b^{P2} }{ \infer{ ° a^{P2} }{ \infer{ ° a^2 }{ [(a\land b)^2]^1 } & a^P } & \infer{ ° b^{P2} }{ \infer{ ° b^2 }{ [(a\land b)^2]^1 } & b^P } } } } } \defded{param-listdef}{ \infer[\eta]{ ° a^{[\;]P} }{ \infer[1]{ ° a^{[\;] 2}\to a^{[\;]P2} }{ \infer={ ° a^{[\;]P2} }{ [a^{[\;] 2}]^1 & a^P } } } } \defded{param-todef}{ \infer[\eta]{ ° (a\to b)^P }{ \infer[3]{ ° (a\to b)^2\to ìa^2.(a^{P2}\to b^{P2}) }{ \infer[1]{ ° ìa^2.(a^{P2}\to b^{P2}) }{ \infer{ ° a^{P2}\to b^{P2} }{ \infer{ ° a^{P2} }{ [a^2]^1 & a^P } & \infer{ ° b^{P2} }{ \infer{ ° b^2 }{ [a^2]^1 & [(a\to b)^2]^3 } & b^P } } } } } } \defded{param-polidef}{ \infer[\eta]{ ° (a\TO a^F)^P }{ \infer[4]{ ° (a\TO a^F)^2\to ì\T_{a^2}.ìa^P.a^{FP2} }{ \infer[3]{ ° ì\T_{a^2}.ìa^P.a^{FP2} }{ \infer[1]{ ° ìa^P.a^{FP2} }{ \infer{ ° a^{FP2} }{ \infer{ ° a^{F2} }{ [\T_{a^2}]^3 & [(a\TO a^F)^2]^4 } & \infer={ ° a^{FP} }{ [a^P]^1 } } } } } } } \defded{param-map1}{ \infer=[1]{ ° (a\TO b\TO ((a\to b)\to (a^{[\;]}\to b^{[\;]})))^P }{ [\T_{a^2}]^1 & [(a\TO \ldots)^2]^1 & \infer=[3]{ ° (b\TO ((a\to b)\to (a^{[\;]}\to b^{[\;]})))^P }{ [\T_{b^2}]^3 & [(b\TO \ldots)^2]^3 & \infer={ ° ((a\to b)\to (a^{[\;]}\to b^{[\;]}))^P }{ \infer={ ° (a\to b)^P }{ [a^P]^1 & [b^P]^2 } & \infer={ ° (a^{[\;]}\to b^{[\;]})^P }{ \infer={ ° a^{[\;]P} }{ [a^P]^1 } & \infer={ ° b^{[\;]P} }{ [b^P]^2 } } } } } } \defded{tat1}{ \infer{ ° h(x,f(x)) }{ \infer{ ° (x,f(x)) }{ x & \infer{ ° f(x) }{ x & f } } & h } } \defded{tat1-t}{ \infer{ ° z }{ \infer{ ° x\land y }{ x & \infer{ ° y }{ x & x\to y } } & x\land y\to z } } \defded{tat2}{ \infer{ ° h(w(t),f(w(t))) }{ \infer{ ° w(t) }{ t & w } & \infer{ ° Ðx.h(x,f(x)) }{ \infer{ ° h(x,f(x)) }{ \infer{ ° (x,f(x)) }{ [x]^1 & \infer{ ° f(x) }{ [x]^1 & f } } & h } } } } \defded{tat2-t}{ \infer{ ° z }{ \infer{ ° x }{ t & t\to x } & \infer[1]{ ° x\to z }{ \infer{ ° z }{ \infer{ ° x\land y }{ [x]^1 & \infer{ ° y }{ [x]^1 & x\to y } } & x\land y\to z } } } } \defded{tat3}{ \infer{ ° h(w(t),f(w(t))) }{ \infer{ ° (w(t),f(w(t))) }{ \infer{ ° w(t) }{ t & w } & \infer{ ° f(w(t)) }{ \infer{ ° w(t) }{ t & w } & f } } & h } } \defded{tat3-t}{ \infer{ ° z }{ \infer{ ° x\land y }{ \infer{ ° x }{ t & t\to x } & \infer{ ° y }{ \infer{ ° x }{ t & t\to x } & x\to y } } & x\land y\to z } } \defded{tat-d1}{ \infer[D]{ ° (\ddx\phi(x))(x_0) }{ x_0 & \phi & \ldots } } \defded{tat-d1t}{ \infer[D]{ ° y_x }{ x & x\to y & \ldots } } \defded{tat-dtot1t}{ \infer{ ° z_{xy} }{ \infer{ ° y }{ x & x\to y } & \infer[2]{ ° y\to z_x }{ \infer{ ° z_x }{ x & \infer[1]{ ° x\to z }{ \infer{ ° z }{ \infer{ ° x\land y }{ [x]^1 & [y]^2 } & x\land y\to z } } } } } } \endinput