Mrthfx

How could we fake a moon landing now?

Can melee weapons be used to deliver Contact Poisons?

What does this Jacques Hadamard quote mean?

Is safe to use va_start macro with this as parameter?

Crossing US/Canada Border for less than 24 hours

How to answer "Have you ever been terminated?"

How to compare two different files line by line in unix?

When a candle burns, why does the top of wick glow if bottom of flame is hottest?

Trademark violation for app?

Quick way to create a symlink?

What does the "x" in "x86" represent?

For a new assistant professor in CS, how to build/manage a publication pipeline

How would a mousetrap for use in space work?

Fantasy story; one type of magic grows in power with use, but the more powerful they are, they more they are drawn to travel to their source

Delete nth line from bottom

What is the escape velocity of a neutron particle (not neutron star)

Significance of Cersei's obsession with elephants?

Most bit efficient text communication method?

Is there any way for the UK Prime Minister to make a motion directly dependent on Government confidence?

Why do the resolve message appear first?

What is the longest distance a player character can jump in one leap?

When the Haste spell ends on a creature, do attackers have advantage against that creature?

First console to have temporary backward compatibility

Wu formula for manifolds with boundary

Bussproofs compact prooftree

0

I have the following code:

begin{prooftree}

    AxiomC{$Gamma $}

    AxiomC{}

    LeftLabel{($to$-elim)}

    BinaryInfC{$Gamma , x : A, y : C vdash x y Leftarrow D$}

    AxiomC{}

    LeftLabel{($equiv_{mathsf{type}}$-refl)}

    UnaryInfC{$Gamma , x : A, y : C vdash D equiv D$}

    LeftLabel{(switch)}

    BinaryInfC{$Gamma , x : A , y : C vdash xy Rightarrow D$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma , x : A vdash lamba y . x y Leftarrow C to D$}

    AxiomC{}

    LeftLabel{$(**)$}

    UnaryInfC{$Gamma , x : A vdash B equiv C to D  mathsf{type}$}

    LeftLabel{(switch)}

    BinaryInfC{$ Gamma , x : A vdash lambda y . xy Rightarrow B$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma vdash lambda x . lambda y . x y Leftarrow A to B$}

    AxiomC{}

    RightLabel{$(*)$}

    UnaryInfC{$Gamma vdash T equiv A to B  mathsf{type}$}

    RightLabel{(switch)}

    BinaryInfC{$Gamma vdash lambda x . lambda y . x y Rightarrow T$}

end{prooftree}

Which gives me the following tree:

Is there a way I can get rid of the whitespace in the middle? Where (*) and (**) take place it would be nice to slide them under the tree. I don't think this is possible in bussproofs from what I have read but I could be wrong.

For example if there is a local horizontal spacing when I do a BinaryInfC that I could change that might let me squish them together.

horizontal-alignment bussproofs

share|improve this question

asked 11 mins ago

Ali CaglayanAli Caglayan

238137

add a comment | 

0

I have the following code:

begin{prooftree}

    AxiomC{$Gamma $}

    AxiomC{}

    LeftLabel{($to$-elim)}

    BinaryInfC{$Gamma , x : A, y : C vdash x y Leftarrow D$}

    AxiomC{}

    LeftLabel{($equiv_{mathsf{type}}$-refl)}

    UnaryInfC{$Gamma , x : A, y : C vdash D equiv D$}

    LeftLabel{(switch)}

    BinaryInfC{$Gamma , x : A , y : C vdash xy Rightarrow D$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma , x : A vdash lamba y . x y Leftarrow C to D$}

    AxiomC{}

    LeftLabel{$(**)$}

    UnaryInfC{$Gamma , x : A vdash B equiv C to D  mathsf{type}$}

    LeftLabel{(switch)}

    BinaryInfC{$ Gamma , x : A vdash lambda y . xy Rightarrow B$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma vdash lambda x . lambda y . x y Leftarrow A to B$}

    AxiomC{}

    RightLabel{$(*)$}

    UnaryInfC{$Gamma vdash T equiv A to B  mathsf{type}$}

    RightLabel{(switch)}

    BinaryInfC{$Gamma vdash lambda x . lambda y . x y Rightarrow T$}

end{prooftree}

Which gives me the following tree:

Is there a way I can get rid of the whitespace in the middle? Where (*) and (**) take place it would be nice to slide them under the tree. I don't think this is possible in bussproofs from what I have read but I could be wrong.

For example if there is a local horizontal spacing when I do a BinaryInfC that I could change that might let me squish them together.

horizontal-alignment bussproofs

share|improve this question

asked 11 mins ago

Ali CaglayanAli Caglayan

238137

add a comment | 

I have the following code:

begin{prooftree}

    AxiomC{$Gamma $}

    AxiomC{}

    LeftLabel{($to$-elim)}

    BinaryInfC{$Gamma , x : A, y : C vdash x y Leftarrow D$}

    AxiomC{}

    LeftLabel{($equiv_{mathsf{type}}$-refl)}

    UnaryInfC{$Gamma , x : A, y : C vdash D equiv D$}

    LeftLabel{(switch)}

    BinaryInfC{$Gamma , x : A , y : C vdash xy Rightarrow D$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma , x : A vdash lamba y . x y Leftarrow C to D$}

    AxiomC{}

    LeftLabel{$(**)$}

    UnaryInfC{$Gamma , x : A vdash B equiv C to D  mathsf{type}$}

    LeftLabel{(switch)}

    BinaryInfC{$ Gamma , x : A vdash lambda y . xy Rightarrow B$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma vdash lambda x . lambda y . x y Leftarrow A to B$}

    AxiomC{}

    RightLabel{$(*)$}

    UnaryInfC{$Gamma vdash T equiv A to B  mathsf{type}$}

    RightLabel{(switch)}

    BinaryInfC{$Gamma vdash lambda x . lambda y . x y Rightarrow T$}

end{prooftree}

Which gives me the following tree:

Is there a way I can get rid of the whitespace in the middle? Where (*) and (**) take place it would be nice to slide them under the tree. I don't think this is possible in bussproofs from what I have read but I could be wrong.

For example if there is a local horizontal spacing when I do a BinaryInfC that I could change that might let me squish them together.

horizontal-alignment bussproofs

share|improve this question

asked 11 mins ago

Ali CaglayanAli Caglayan

238137

begin{prooftree}

    AxiomC{$Gamma $}

    AxiomC{}

    LeftLabel{($to$-elim)}

    BinaryInfC{$Gamma , x : A, y : C vdash x y Leftarrow D$}

    AxiomC{}

    LeftLabel{($equiv_{mathsf{type}}$-refl)}

    UnaryInfC{$Gamma , x : A, y : C vdash D equiv D$}

    LeftLabel{(switch)}

    BinaryInfC{$Gamma , x : A , y : C vdash xy Rightarrow D$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma , x : A vdash lamba y . x y Leftarrow C to D$}

    AxiomC{}

    LeftLabel{$(**)$}

    UnaryInfC{$Gamma , x : A vdash B equiv C to D  mathsf{type}$}

    LeftLabel{(switch)}

    BinaryInfC{$ Gamma , x : A vdash lambda y . xy Rightarrow B$}

    LeftLabel{($to$-intro)}

    UnaryInfC{$Gamma vdash lambda x . lambda y . x y Leftarrow A to B$}

    AxiomC{}

    RightLabel{$(*)$}

    UnaryInfC{$Gamma vdash T equiv A to B  mathsf{type}$}

    RightLabel{(switch)}

    BinaryInfC{$Gamma vdash lambda x . lambda y . x y Rightarrow T$}

end{prooftree}

share|improve this question

asked 11 mins ago

Ali CaglayanAli Caglayan

238137

share|improve this question

asked 11 mins ago

Ali CaglayanAli Caglayan

238137

asked 11 mins ago

Ali CaglayanAli Caglayan

238137

asked 11 mins ago

Ali CaglayanAli Caglayan

238137