One is for a proof by cases; it accepts a disjunction ("or") as input, gives you a local branch for each disjoined option, and hopes you'll show that each branch individually proves P. Then the block globally proves P. This one was intuitive to me.
One is for instantiating variables from existential quantifiers. If you send ∃x.P(x) into that block's global input, you will get P(c), where c is a constant, coming out of that block's local output. You're supposed to prove an expression that does not involve c, send that to local input, and get it back out of global output.
As far as I can tell, this is done for reasons of convenient implementation. Mathematically, the notch shouldn't be there at all -- you should just be able to hook up ∃x.P(x) to global input, and get P(c) on global output. But I think the tool author wants to think of c as being a variable which is scoped inside the ∃-instantiation block and can't exist outside it.
One is for a proof by cases; it accepts a disjunction ("or") as input, gives you a local branch for each disjoined option, and hopes you'll show that each branch individually proves P. Then the block globally proves P. This one was intuitive to me.
One is for instantiating variables from existential quantifiers. If you send ∃x.P(x) into that block's global input, you will get P(c), where c is a constant, coming out of that block's local output. You're supposed to prove an expression that does not involve c, send that to local input, and get it back out of global output.
As far as I can tell, this is done for reasons of convenient implementation. Mathematically, the notch shouldn't be there at all -- you should just be able to hook up ∃x.P(x) to global input, and get P(c) on global output. But I think the tool author wants to think of c as being a variable which is scoped inside the ∃-instantiation block and can't exist outside it.