Concatenation and contraposition laws in modified Stalnaker system The first four axioms of Stalnaker conditional logic, which adds $\mapsto$, the counterfactual conditional symbol, to the operator symbols of classical logic, are


*

*$A\mapsto A$

*$(A\mapsto B)\rightarrow(A\rightarrow B)$

*$(\lnot A\mapsto A)\rightarrow (B\mapsto A)$

*$((A\mapsto B)\land(B\mapsto A))\rightarrow((A\mapsto C)\leftrightarrow(B\mapsto C))$


The inference system uses two inference rules (together with the rules of classical logic for the truth-functional symbols, I think, although the text I am following -see below- explicitly tells nothing about that):


*

*$A\leftrightarrow B\vdash(C\mapsto A)\leftrightarrow(C\mapsto B) $

*$A_1\land\ldots\land A_n\rightarrow B\vdash (C\mapsto A_1)\land\ldots\land (C\mapsto A_n)\rightarrow(C\mapsto B)\quad\quad\quad(n\ge 0)$


I read -D. Palladino, C. Palladino, Logiche non classiche, 'non-classical logics', 2007, p. 122, for anybody having the book- that adding the following axiom$$(A\lor B\mapsto C)\leftrightarrow (A\mapsto C)\land (B\mapsto C)$$to the above rules and four axioms would make the the contraposition law $(\lnot A\mapsto\lnot B)\rightarrow(B\mapsto  A)$ and the concatenation law $(A\mapsto B)\rightarrow((B\mapsto C)\rightarrow(A\mapsto C))$ valid (which usually is not desired in conditional logic), but I am not able to prove it to myself. How can they be inferred? I heartily thank you for any answer!
EDIT: An answer to this question by a kind fellow MSE user, whom I thank very much, does exist, but presents a problem, as noticed both by the answerer and another user, since it does not use axiom $(A\lor B\mapsto C)\leftrightarrow (A\mapsto C)\land (B\mapsto C)$, in particular the $(A\lor B\mapsto C)\rightarrow (A\mapsto C)\land (B\mapsto C)$ part, which is indispensable to prove the concatenation and contraposition laws, which are not valid in absence of that axiom. Indeed, $(A\lor B\mapsto C)\rightarrow (A\mapsto C)\land (B\mapsto C)$ is usually left out of conditional logic systems, where the concatenation and contraposition laws are not desired.
 A: Contraposition: $(\neg A\mapsto\neg B)\to(B\mapsto A)$
We start with the tautology: $(B\to A)\to(B\to A)$.
Contraposition of the premise yields: $(\neg A\to\neg B)\to(B\to A)$.
Contraposition of the whole formula yields: $\neg(B\to A)\to\neg(\neg A\to\neg B)$.
By the contrapositive of axiom 2, this is equivalent to: $\neg(B\mapsto A)\to\neg(\neg A\mapsto\neg B)$.
Finally, by contraposition of the whole formula: $(\neg A\mapsto\neg B)\to(B\mapsto A)$.

Concatenation: $(A\mapsto B)\to((B\mapsto C)\to(A\mapsto C))$
We start with the tautology: $(A\to B)\to((B\to C)\to(A\to C))$.
Contraposition yields: $\neg((B\to C)\to(A\to C))\to\neg(A\to B)$.
Distributing the negation into the implication: $((B\to C)\land\neg(A\to C))\to\neg(A\to B)$.
By the contrapositive of axiom 2, this is equivalent to: $((B\to C)\land\neg(A\mapsto C))\to\neg(A\mapsto B)$.
Extraction of the negation gives: $\neg(\neg(B\to C)\lor(A\mapsto C))\to\neg(A\mapsto B)$.
By the contrapositive of axiom 2, this is equivalent to: $\neg(\neg(B\mapsto C)\lor(A\mapsto C))\to\neg(A\mapsto B)$.
Rewriting the premise as an implication: $\neg((B\mapsto C)\to(A\mapsto C))\to\neg(A\mapsto B)$.
Finally, contraposition yields: $(A\mapsto B)\to((B\mapsto C)\to(A\mapsto C))$.
A: Contraposition. Want to show $(\neg A\mapsto\neg B)\to(B\mapsto A)$.


*

*Assume $(\neg A \mapsto \neg B) \land \neg(B \mapsto A)$, looking for contradiction.

*By axiom 2, $\neg A \rightarrow \neg B$, or equivalently $A \lor \neg B$

*New axiom letting $C = A$. $(A \lor B\mapsto A)\leftrightarrow (A \mapsto A)\land (B\mapsto A)$

*By axiom 1, $(A \lor B\mapsto A)\leftrightarrow (B\mapsto A)$
If $A$ is true then $B$ is irrelevant on the left hand side and therefore $(B \mapsto A)$, a contradiction.
If $A$ is false, then $B$ must also be false by 2, and therefore $B = A$. So by axiom 1 $(B \mapsto A)$, a contradiction.

Concatenation. Want to show $(A\mapsto B)\rightarrow((B\mapsto C)\rightarrow(A\mapsto C))$


*

*Assume $(A \mapsto B) \land \neg ((B \mapsto C) \rightarrow (A \mapsto C))$. Looking for contradiction.

*Equivalently, $(A \mapsto B) \land (B \mapsto C) \land \neg(A \mapsto C)$.

*New axiom $(A \lor B \mapsto C) \leftrightarrow (A \mapsto C) \land (B \mapsto C)$.
Thus it is sufficient to show that $(A \lor B \mapsto C)$.
If $B$ is true, we are done, so continue assuming $B$ is false.


*Axiom 2 and step 2 gives us $A \rightarrow B$. Since $B$ is false, $A$ must also be false. 


Since $(A \mapsto B)$ is true we gather that $(\bot \mapsto \bot)$ must be true.
If $C$ is false then $(A \lor B \mapsto C)$ is $(\bot \lor \bot \mapsto \bot)$ which is true and we are done.
If $C$ is true, note that $(B \mapsto C)$ is true, therefore $(\bot \mapsto \top)$ is true, and therefore $(A \lor B \mapsto C)$ is true and we are done.
