@Xima I was just editing the new improved version. :D Let me know if there's something missing or that you don't understand.

@Xima Did you see the new edit?

@Xima I have simplified it further. The nodes at the side are now actually a branch (more consistent).

This is basically what justtrees does automatically, by the way. Adds another branch (or 2 if you want labels on both sides) with no edges, aligned to the levels in the main tree. Which is also why a justtree, unlike a forest need not have a single root: the real root is added automatically but invisibly to allow the branches on each side. But your solution is probably safer (+1) as it does not rely on code by me ;).

@cfr :D actually, your code is fine, but it relies on naming the levels. If I can give a suggestion for improving it, it would be that: try making that automatic :P but I appreciate the work behind it, so here's a (+1) from me too. Oh and your code is safe too :D

@Alenanno I don't understand what you mean about naming the levels. I use tier=terminus in this case to ensure that all the final children are on the same level. What names the levels?

@cfr when you wrote just=<name>, I was referring to that. That's similar to my first solution (see my answers revisions, the first one I think).

@Alenanno See my edit below. If you want a label for that level, you have to tell the style what the label should be. If you don't need a label, you don't have to specify one. I don't understand how that could be automated: how could the code automatically determine the correct content of the label for a level or whether that level should have a label at all?

@cfr got my last comment?

You are naming nodes in your first solution so you can refer to them later to add the labels. I'm not doing that. just=<stuff> tells the style that this level (whatever it happens to be) should get a label with the content <stuff>. If you don't need a label, you don't specify it.

Aahhhhh I got it now

@Alenanno Yes. But I'm not doing that at all.

Yes now I understand

Just= is the label, not the reference

Thanks for the clarification :D

@Alenanno Good ;). I spent a lot of time automating it! The original code is for proof trees with line numbers on the left and justifications on the right. The line numbers can be added automatically, but obviously the justifications vary depending on the logical inference represented in the tree, so the user has to be able to specify their content somehow. So the idea what you can say <logical formular>, just=<inference rule> and the style would number the line and add the label at right.

@Alenanno Yes ;).

@Alenanno Good ;). I spent a lot of time automating it! The original code is for proof trees with line numbers on the left and justifications on the right. The line numbers can be added automatically, but obviously the justifications vary depending on the logical inference represented in the tree, so the user has to be able to specify their content somehow. So the idea what you can say <logical formula>, just=<inference rule> and the style would number the line and add the label at right.

Sorry. Didn't mean to send that twice.

Lol it's ok :D