[Question]
  [
Well I think it is about time we have another [proof-golf](/questions/tagged/proof-golf "show questions tagged 'proof-golf'") question.
This time we are going to prove the well known logical truth
\$(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)\$
To do this we will use Łukasiewicz's third [Axiom Schema](https://en.wikipedia.org/wiki/Axiom_schema), an incredibly elegant set of three axioms that are complete over [propositional logic](https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system).
Here is how it works:
# Axioms
The Łukasiewicz system has three axioms. They are:
\$\phi\rightarrow(\psi\rightarrow\phi)\$
\$(\phi\rightarrow(\psi\rightarrow\chi))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\chi))\$
\$(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$
The axioms are universal truths regardless of what we choose for \$\phi\$, \$\psi\$ and \$\chi\$. At any point in the proof we can introduce one of these axioms. When we introduce an axiom you replace each case of \$\phi\$, \$\psi\$ and \$\chi\$, with a "complex expression". A complex expression is any expression made from Atoms, (represented by the letters \$A\$-\$Z\$), and the operators implies (\$\rightarrow\$) and not (\$\neg\$).
For example if I wanted to introduce the first axiom (L.S.1) I could introduce
\$A\rightarrow(B\rightarrow A)\$
or
\$(A\rightarrow A)\rightarrow(\neg D\rightarrow(A\rightarrow A))\$
In the first case \$\phi\$ was \$A\$ and \$\psi\$ was \$B\$, while in the second case both were more involved expressions. \$\phi\$ was \$(A\rightarrow A)\$ and \$\psi\$ was \$\neg D\$.
What substitutions you choose to use will be dependent on what you need in the proof at the moment.
## Modus Ponens
Now that we can introduce statements we need to relate them together to make new statements. The way that this is done in Łukasiewicz's Axiom Schema (L.S) is with Modus Ponens. Modus Ponens allows us to take two statements of the form
\$\phi\$
\$\phi\rightarrow \psi\$
and instantiate a new statement
\$\psi\$
Just like with our Axioms \$\phi\$ and \$\psi\$ can stand in for any arbitrary statement.
The two statements can be anywhere in the proof, they don't have to be next to each other or any special order.
## Task
Your task will be to prove [the law of contrapositives](https://en.wikipedia.org/wiki/Contraposition). This is the statement
\$(A\rightarrow B)\rightarrow(\neg B\rightarrow\neg A)\$
Now you might notice that this is rather familiar, it is an instantiation of the reverse of our third axiom 
\$(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$
However this is no trivial feat.
## Scoring
Scoring for this challenge is pretty simple, each time you instantiate an axiom counts as a point and each use of modus ponens counts as a point. This is essentially the number of lines in your proof. The goal should be to minimize your score (make it as low as possible).
## Example Proof
Ok now lets use this to construct a small proof. We will prove \$A\rightarrow A\$.
Sometimes it is best to work backwards since we know where we want to be we can figure how we might get there. In this case since we want to end with \$A\rightarrow A\$ and this is not one of our axioms we know the last step must be modus ponens. Thus the end of our proof will look like 
```
φ
φ → (A → A)
A → A       M.P.
```
[TeX](https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9ClxwaGlcXApccGhpXHJpZ2h0YXJyb3coQVxyaWdodGFycm93IEEpXFwKQVxyaWdodGFycm93IEEgXHRhZyp7TS5QLn1cXApcZW5ke2dhdGhlcip9.svg)
Where \$\phi\$ is an expression we don't yet know the value of. Now we will focus on \$\phi\rightarrow(A\rightarrow A)\$. This can be introduced either by modus ponens or L.S.3. L.S.3 requires us to prove \$(\neg A\rightarrow\neg A)\$ which seems just as hard as \$(A\rightarrow A)\$, so we will go with modus ponens. So now our proof looks like
```
φ
ψ
ψ → (φ → (A → A))
φ → (A → A)        M.P.
A → A              M.P.
```
[TeX](https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9ClxwaGkgXFwKXHBzaSBcXApccHNpIFxyaWdodGFycm93IChccGhpIFxyaWdodGFycm93CihBIFxyaWdodGFycm93IEEpKVxcClxwaGkgXHJpZ2h0YXJyb3cKKEEgXHJpZ2h0YXJyb3cgQSkgXHRhZyp7TS5QLn1cXApBIFxyaWdodGFycm93IEEgXHRhZyp7TS5QLn1cXApcZW5ke2dhdGhlcip9.svg)
Now \$\psi\rightarrow(\phi\rightarrow(A\rightarrow A))\$ looks a lot like our second axiom L.S.2 so we will fill it in as L.S.2
```
A → χ
A → (χ → A)
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A)                   M.P.
A → A                               M.P.
```
[TeX](https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBIFxyaWdodGFycm93IFxjaGkpIFxcCihBIFxyaWdodGFycm93IChcY2hpIFxyaWdodGFycm93IEEpKSBcXAooQSBccmlnaHRhcnJvdyAoXGNoaSBccmlnaHRhcnJvdyBBKSkKXHJpZ2h0YXJyb3cgKChBIFxyaWdodGFycm93ClxjaGkpXHJpZ2h0YXJyb3cKKEEgXHJpZ2h0YXJyb3cgQSkpIFx0YWcqe0wuUy4yfVxcCihBIFxyaWdodGFycm93IFxjaGkpIFxyaWdodGFycm93CihBIFxyaWdodGFycm93IEEpIFx0YWcqe00uUC59XFwKQSBccmlnaHRhcnJvdyBBIFx0YWcqe00uUC59XFwKXGVuZHtnYXRoZXIqfQ==.svg)
Now our second statement \$(A\rightarrow(\chi\rightarrow A))\$ can pretty clearly be constructed from L.S.1 so we will fill that in as such
```
A → χ
A → (χ → A)                         L.S.1
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A)                   M.P.
A → A                               M.P.
```
[TeX](https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBIFxyaWdodGFycm93IFxjaGkpIFxcCkEgXHJpZ2h0YXJyb3cgKFxjaGkgXHJpZ2h0YXJyb3cgQSkKXHRhZyp7TC5TLjF9XFwKKEEgXHJpZ2h0YXJyb3cgKFxjaGkgXHJpZ2h0YXJyb3cgQSkpClxyaWdodGFycm93ICgoQSBccmlnaHRhcnJvdwpcY2hpKVxyaWdodGFycm93CihBIFxyaWdodGFycm93IEEpKSBcdGFnKntMLlMuMn1cXAooQSBccmlnaHRhcnJvdyBcY2hpKSBccmlnaHRhcnJvdwooQSBccmlnaHRhcnJvdyBBKSBcdGFnKntNLlAufVxcCkEgXHJpZ2h0YXJyb3cgQSBcdGFnKntNLlAufVxcClxlbmR7Z2F0aGVyKn0=.svg)
Now we just need to find a \$\chi\$ such that we can prove \$A\rightarrow\chi\$. This can very easily be done with L.S.1 so we will try that
```
A → (ω → A)                                     L.S.1
A → ((ω → A) → A)                               L.S.1
(A → ((ω → A) → A)) → ((A → (ω → A)) → (A → A)) L.S.2
(A → (ω → A)) → (A → A)                         M.P.
A → A                                           M.P.
```
[TeX](https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBXHJpZ2h0YXJyb3coXG9tZWdhXHJpZ2h0YXJyb3cgQSkpClxcCkFccmlnaHRhcnJvdygoXG9tZWdhXHJpZ2h0YXJyb3cgQSkKXHJpZ2h0YXJyb3cgQSlcdGFnKntMLlMuMX1cXAooQVxyaWdodGFycm93KChcb21lZ2FccmlnaHRhcnJvdyBBKQpccmlnaHRhcnJvdyBBKSlccmlnaHRhcnJvdygoQQpccmlnaHRhcnJvdyhcb21lZ2FccmlnaHRhcnJvdyBBKSkKXHJpZ2h0YXJyb3coQSBccmlnaHRhcnJvdyBBKSkKXHRhZyp7TC5TLjJ9XFwKKEFccmlnaHRhcnJvdyhcb21lZ2FccmlnaHRhcnJvdyBBKSkKXHJpZ2h0YXJyb3cKKEFccmlnaHRhcnJvdyBBKVx0YWcqe00uUC59XFwKQVxyaWdodGFycm93IEFcdGFnKntNLlAufVxcClxlbmR7Z2F0aGVyKn0=.svg)
Now since all of our steps our justified we can fill in \$\omega\$, as any statement we want and the proof will be valid. We could choose \$A\$ but I will choose \$B\$ so that it is clear that it doesn't need to be \$A\$.
```
A → (B → A)                                     L.S.1
A → ((B → A) → A)                               L.S.1
(A → ((B → A) → A)) → ((A → (B → A)) → (A → A)) L.S.2
(A → (B → A)) → (A → A)                         M.P.
A → A                                           M.P.
```
[TeX](https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBXHJpZ2h0YXJyb3coQlxyaWdodGFycm93IEEpKQpcdGFnKntMLlMuMX1cXApBXHJpZ2h0YXJyb3coKEJccmlnaHRhcnJvdyBBKQpccmlnaHRhcnJvdyBBKVx0YWcqe0wuUy4xfVxcCihBXHJpZ2h0YXJyb3coKEJccmlnaHRhcnJvdyBBKQpccmlnaHRhcnJvdyBBKSlccmlnaHRhcnJvdygoQQpccmlnaHRhcnJvdyhCXHJpZ2h0YXJyb3cgQSkpClxyaWdodGFycm93KEEgXHJpZ2h0YXJyb3cgQSkpClx0YWcqe0wuUy4yfVxcCihBXHJpZ2h0YXJyb3coQlxyaWdodGFycm93IEEpKQpccmlnaHRhcnJvdwooQVxyaWdodGFycm93IEEpXHRhZyp7TS5QLn1cXApBXHJpZ2h0YXJyb3cgQVx0YWcqe00uUC59XFwKXGVuZHtnYXRoZXIqfQ==.svg)
[Try it online!](https://tio.run/##hVVta9swEP7uX6EZRiR2NkvzrVsLzmB0kNEy94NLElxvURqDIxtbTTay/vbszrLrl7gZAUd67nnuRbqzszxN0ien2MfHY6TTLZ/f/L1fCuY412x@s4TDr3QlQ/0nk/wGoiTbROIFSuK9cK1K8R@@a1n7wjCWbr3kNrM/2QttC9gXyFCp5oHxYzs2YlDoSMutVDpEAzLiNQ/gwVA6NiLbznVf9ICi92@IHozo83Ck1r6sMBDGQbVx2wSTt7Gbdcdcxa8K42W4CiszEHaHHnSIp1USveF3vXc8t7zWTgccorOf0SpsqPP6KvGiepag6YsA7zlYXI0/vkCXRD1hJcW4DnkIrjAlj/IKwRPYOu2sXKRedKk1ewpfhIAamJZLj7ABF5MTF3QPngD6mxo306HoVi4LHabrMImVfK2MHfDJFlfscaEeX4C1Se6pxF4oupMsj/FUCy0z7uutBh9Xgl06LNvkUSF5E5nMApivc3xSR4U0MgWWV0L7PNaSst9GWRIXmpeA8QcqgXcYbBcl8coECyA0xZtTB0oHDq1sAmDzEZv549GSJnFYenFWenFOOjkrnQxI/d40Ng6U3oz5D7m71RvwzZXjaEENewrPFS8SEqme9Ib7MBOAXBYXbPZh7FRKpLUQEp0k9v2OjUgJI/wh4836BpI8cfZNlUpGkCkXuyFN17wqtFc8MGPFgfKX2IUdLs04RanBnrk7ba8ptbro9llDUHcRbqplojhWHSXrNN/KVVPWCIeiHytsXgGE7GROfZxLjL2OE3y5p1Us241V9qxdHac23JEW8P2BTZ1lUq24QWiK4Gv8W67KPZVvJqI6BRK0zBjz0jFRXet49Bh9Kqb09IRldvW2AvkQKgzWkRvMqzbWGaMJ5P0D "Prolog (SWI) - Proof Verifier")
And that is a proof.
## Resources
### Verification program
[Here](https://tio.run/##hVVta9swEP7uX6EZRiR2NkvzrVsLzmB0kNEy94NLElxvURqDIxtbTTay/vbszrLrl7gZAUd67nnuRbqzszxN0ien2MfHY6TTLZ/f/L1fCuY412x@s4TDr3QlQ/0nk/wGoiTbROIFSuK9cK1K8R@@a1n7wjCWbr3kNrM/2QttC9gXyFCp5oHxYzs2YlDoSMutVDpEAzLiNQ/gwVA6NiLbznVf9ICi92@IHozo83Ck1r6sMBDGQbVx2wSTt7Gbdcdcxa8K42W4CiszEHaHHnSIp1USveF3vXc8t7zWTgccorOf0SpsqPP6KvGiepag6YsA7zlYXI0/vkCXRD1hJcW4DnkIrjAlj/IKwRPYOu2sXKRedKk1ewpfhIAamJZLj7ABF5MTF3QPngD6mxo306HoVi4LHabrMImVfK2MHfDJFlfscaEeX4C1Se6pxF4oupMsj/FUCy0z7uutBh9Xgl06LNvkUSF5E5nMApivc3xSR4U0MgWWV0L7PNaSst9GWRIXmpeA8QcqgXcYbBcl8coECyA0xZtTB0oHDq1sAmDzEZv549GSJnFYenFWenFOOjkrnQxI/d40Ng6U3oz5D7m71RvwzZXjaEENewrPFS8SEqme9Ib7MBOAXBYXbPZh7FRKpLUQEp0k9v2OjUgJI/wh4836BpI8cfZNlUpGkCkXuyFN17wqtFc8MGPFgfKX2IUdLs04RanBnrk7ba8ptbro9llDUHcRbqplojhWHSXrNN/KVVPWCIeiHytsXgGE7GROfZxLjL2OE3y5p1Us241V9qxdHac23JEW8P2BTZ1lUq24QWiK4Gv8W67KPZVvJqI6BRK0zBjz0jFRXet49Bh9Kqb09IRldvW2AvkQKgzWkRvMqzbWGaMJ5P0D "Prolog (SWI) - Proof Verifier") is a Prolog program you can use to verify that your proof is in fact valid. Each step should be placed on its own line. `->` should be used for implies and `-` should be used for not, atoms can be represented by any string of alphabetic characters.
### Metamath
[Metamath](http://us.metamath.org) uses the Łukasiewicz system for its proofs in propositional calculus, so you may want to poke around there a bit. They also have a proof of the theorem this challenge asks for which can be found [here](http://us.metamath.org/mpeuni/con3.html). There is an explanation [here](http://us.metamath.org/mpeuni/mmset.html#proofs) of how to read the proofs.
### The Incredible Proof Machine
@[Antony](https://codegolf.stackexchange.com/users/71303/antony) made me aware of a tool called [The Incredible Proof machine](http://incredible.pm/) which allows you to construct proofs in a number of systems using a nice graphical proof system. If you scroll down you will find they support the Łukasiewicz system. So if you are a more visual oriented person you can work on your proof there. Your score will be the number of blocks used minus 1.
  
[Answer]
# ~~88~~ ~~82~~ ~~77~~ 72 steps
Thanks to H.PWiz for better combinator conversions that saved 10 steps!
### Explanation
You might be familiar with the [Curry–Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence), in which theorems correspond to types and proofs correspond to programs of those types. The first two axioms in the Łukasiewicz system are actually the [K and S combinators](https://en.wikipedia.org/wiki/SK_combinator_calculus), and it’s well known that we can [translate](https://codegolf.stackexchange.com/q/105991/39242) lambda calculus expressions into the SK combinatory expressions.
So let’s write down some expressions corresponding to our axioms (the following is valid Haskell syntax, which is convenient because we can quite literally check our proofs using the Haskell compiler):
```
data Not φ
k :: φ -> (ψ -> φ)
k x _ = x
s :: (φ -> (ψ -> χ)) -> ((φ -> ψ) -> (φ -> χ))
s x y z = x z (y z)
c :: (Not φ -> Not ψ) -> (ψ -> φ)
c = error "non-computational axiom"
```
Then we can write a proof of the desired statement as a program in terms of `c` (this part takes a bit of cleverness, but it’s much easier to write this than an 72-line axiomatic proof):
```
pf :: (a -> b) -> (Not b -> Not a)
pf x y = c (\z -> c (\_ -> y) (x (c (c (\_ -> z)) x))) k
```
and convert it into an SK combinatory expression:
```
pf' :: (a -> b) -> (Not b -> Not a)
pf' =
  s (k (s (k (s c (k k)))))
    (s (k (s (s (k s) (s (k k) (s (k c) k)))))
       (s (k k) (s (k (s s (s (s (k c) (s (k c) k))))) k)))
```
The 17 `k`, 16 `s`, and 4 `c` combinators above correspond to the 16 LS1, 16 LS2, and 4 LS3 invocations in the proof below, and the 38 applications of a function to a value above correspond to the 38 MP invocations below.
Why only 16 LS1 invocations? It turns out one of the `k` combinators above has a free type variable, and instantiating it carefully turns it into a duplicate of another one that has already been derived.
### The proof
1. (A → B) → (¬¬A → (A → B)) LS1
2. ¬¬A → (¬¬(A → B) → ¬¬A) LS1
3. (¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)) LS3
4. ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B))) → (¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)))) LS1
5. ¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B))) MP 4,3
6. (¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → (¬¬A → (¬A → ¬(A → B)))) LS2
7. (¬¬A → (¬¬(A → B) → ¬¬A)) → (¬¬A → (¬A → ¬(A → B))) MP 6,5
8. ¬¬A → (¬A → ¬(A → B)) MP 7,2
9. (¬A → ¬(A → B)) → ((A → B) → A) LS3
10. ((¬A → ¬(A → B)) → ((A → B) → A)) → (¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A))) LS1
11. ¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A)) MP 10,9
12. (¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A))) → ((¬¬A → (¬A → ¬(A → B))) → (¬¬A → ((A → B) → A))) LS2
13. (¬¬A → (¬A → ¬(A → B))) → (¬¬A → ((A → B) → A)) MP 12,11
14. ¬¬A → ((A → B) → A) MP 13,8
15. (¬¬A → ((A → B) → A)) → ((¬¬A → (A → B)) → (¬¬A → A)) LS2
16. (¬¬A → (A → B)) → (¬¬A → A) MP 15,14
17. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)) LS2
18. ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) → (((¬¬A → (A → B)) → (¬¬A → A)) → ((¬¬A → (A → B)) → (¬¬A → B))) LS2
19. ((¬¬A → (A → B)) → (¬¬A → A)) → ((¬¬A → (A → B)) → (¬¬A → B)) MP 18,17
20. (¬¬A → (A → B)) → (¬¬A → B) MP 19,16
21. ((¬¬A → (A → B)) → (¬¬A → B)) → ((A → B) → ((¬¬A → (A → B)) → (¬¬A → B))) LS1
22. (A → B) → ((¬¬A → (A → B)) → (¬¬A → B)) MP 21,20
23. ((A → B) → ((¬¬A → (A → B)) → (¬¬A → B))) → (((A → B) → (¬¬A → (A → B))) → ((A → B) → (¬¬A → B))) LS2
24. ((A → B) → (¬¬A → (A → B))) → ((A → B) → (¬¬A → B)) MP 23,22
25. (A → B) → (¬¬A → B) MP 24,1
26. (¬¬A → B) → (¬B → (¬¬A → B)) LS1
27. ((¬¬A → B) → (¬B → (¬¬A → B))) → ((A → B) → ((¬¬A → B) → (¬B → (¬¬A → B)))) LS1
28. (A → B) → ((¬¬A → B) → (¬B → (¬¬A → B))) MP 27,26
29. ((A → B) → ((¬¬A → B) → (¬B → (¬¬A → B)))) → (((A → B) → (¬¬A → B)) → ((A → B) → (¬B → (¬¬A → B)))) LS2
30. ((A → B) → (¬¬A → B)) → ((A → B) → (¬B → (¬¬A → B))) MP 29,28
31. (A → B) → (¬B → (¬¬A → B)) MP 30,25
32. ¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) LS1
33. (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) LS3
34. ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS1
35. ¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 34,33
36. (¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B)) → (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS2
37. (¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B)) → (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 36,35
38. ¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) MP 37,32
39. (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) LS1
40. ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
41. ¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 40,39
42. (¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → ((¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
43. (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 42,41
44. ¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 43,38
45. (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) LS2
46. ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
47. ¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 46,45
48. (¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → ((¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
49. (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 48,47
50. ¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 49,44
51. (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS2
52. (¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 51,50
53. ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
54. (A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 53,52
55. ((A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → (((A → B) → (¬B → (¬¬A → B))) → ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
56. ((A → B) → (¬B → (¬¬A → B))) → ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 55,54
57. (A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 56,31
58. (¬¬A → (¬¬(A → B) → ¬¬A)) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) LS1
59. (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A)) MP 58,2
60. (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → ¬A) LS3
61. ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → ¬A)) → (((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) LS2
62. ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) MP 61,60
63. (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A MP 62,59
64. ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) → (¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) LS1
65. ¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) MP 64,63
66. (¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) LS2
67. (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A) MP 66,65
68. ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) → ((A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A))) LS1
69. (A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) MP 68,67
70. ((A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A))) → (((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → (¬B → ¬A))) LS2
71. ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → (¬B → ¬A)) MP 70,69
72. (A → B) → (¬B → ¬A) MP 71,57
[Try it online!](https://tio.run/##xVhbb6NGFH4/v2KKVBnUAdXJ27ZZya5UpVKqXdX7QBRbLK3xGgkDMrNJq2x@e3qGgcDg4WrwKpIDZ77vO5c5c7HjYxREX8zkyX99dVl00B9uv33aGMQ035OH2w19/ifaeg77L/b0W@oG8d41XmgK/GRYkDFa8BbAUyIQGyt/1DWi/aKtmWbQpwQRYcR0W@hopoY2mjCXeQcvZA4OIMLf6Ta9FxBpjIM1832VdI@kH2tI94L0q9pT6T3N0DaEQPZilQEibjEunqXhzH@WmJ66y2xpBIYmwW0JeJolhxd4WV1SLqnmogpBFPvb3ToF9CGfSpyoyohd9IWN82yvb@Y/v1AZxHsCgmSeu3y2bzCkBY/LoQsDW6cclYXQKxmao5f0N8OguWGZPi64TSFxfSLB52FhUP5vKWSWKu9w9BLmRDsn8EPvLTPyjJ9kfUM@r8PPL5SUQdYpRVuHfE7io49VTZgX6yt2YHSFTwZ5Z5J4f3QTTy8882GDkhU74ifvKIcvmQTTS01PR595PPqDGwd@wvTUIPRoGNAf0NmjG/hb4cymjkheVJ3ycOhzKRqbkocZuVvNZxu@EtXUq0bqVRP1upF6raCuKquxEAjZfq7/5T1@YHu6ElOOS4vm5kWIdcWJpIEXfmF7fUXvDIpY4ifk7qe5mTERVrJw0klgf34kM86kM/xDRG1@iiBPxP4IUybhJpEudkMU7fQs0UrylIhRXFCrDXahhOVrnHvJjZVhebW9hVTqog9fGbXzLsKX7DEIdczaDXbR8eBti7RmuCiqvpxiC@CWR@/I@/jooe@dH@DmHmW@NMsP46/MYn6k0Y@cS3H/wKaOYy/c6sLCVxH93f/X26bvPH2xIrIqcEJpGH2@M4VXC15f9QXBUJYG/9RNM33LbQbkBtMs49BqgMImoKnRLDT0rkg5hs6sIsrOFBjgJYfXFUSOXhHlcC7UjcCJRURZkl@kE9COqha/A6Nc@A5w6KleKXhzs1QjG8YDtR3q8HKIUjaZUcpbDagZLwBleL6g@hCy4bY425MRS2cUHWgBQKvCyXx0ib0PHHqqZ1Vu2k8VQculHUwGtR2KRzGwrG2mOkRDoWspNZWuxUNf/fpaKztDGeEZbGgehzdL255viinqAEuHl2Iva0Bnx@14elKKI0u/FWpkXZgq3ky0x@xK5etWk2n1oTsWuoCkrarb5EwiK/fpJB6Kdp1EHiaOXmreviu/Z6Eu4gYGkKAXWnka5TfKti6/jKPq/nwRn@WN@yIO4eIZVrb6oRvRwPJ@J8dwDhvO860q@FK5O/Q4QYerwDixqC7PI8ieXLBHKdsEcaou6h2@YfSuxsQeYDi3/XefbkLyT0TK69ooOn1kWi@oi9JBOI5e5ceMM2vWs/6iPt/NN/RBQz9t1eHRsSBDWDDMl2pn6n69zNp7OBvO8916GPSTaz4E@pZlxLhaN/3@p6aU9UTKoLb/Dw "Prolog (SWI) – Try It Online")
[Answer]
# 91 Steps
Full Proof:
```
1. (A → B) → (¬¬A → (A → B)) LS1
2. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)) LS2
3. ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) → ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) LS1
4. (A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) MP 3,2
5. ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) → (((A → B) → (¬¬A → (A → B))) → ((A → B) → ((¬¬A → A) → (¬¬A → B)))) LS2
6. ((A → B) → (¬¬A → (A → B))) → ((A → B) → ((¬¬A → A) → (¬¬A → B))) MP 5,4
7. (A → B) → ((¬¬A → A) → (¬¬A → B)) MP 6,1
8. ¬A → (¬¬(B → (¬A → A)) → ¬A) LS1
9. (¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))) LS3
10. ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A)))) → (¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))))) LS1
11. ¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A)))) MP 10,9
12. (¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))))) → ((¬A → (¬¬(B → (¬A → A)) → ¬A)) → (¬A → (A → ¬(B → (¬A → A))))) LS2
13. (¬A → (¬¬(B → (¬A → A)) → ¬A)) → (¬A → (A → ¬(B → (¬A → A)))) MP 12,11
14. ¬A → (A → ¬(B → (¬A → A))) MP 13,8
15. (¬A → (A → ¬(B → (¬A → A)))) → ((¬A → A) → (¬A → ¬(B → (¬A → A)))) LS2
16. (¬A → A) → (¬A → ¬(B → (¬A → A))) MP 15,14
17. (¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A) LS3
18. ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A)) → ((¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A))) LS1
19. (¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A)) MP 18,17
20. ((¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A))) → (((¬A → A) → (¬A → ¬(B → (¬A → A)))) → ((¬A → A) → ((B → (¬A → A)) → A))) LS2
21. ((¬A → A) → (¬A → ¬(B → (¬A → A)))) → ((¬A → A) → ((B → (¬A → A)) → A)) MP 20,19
22. (¬A → A) → ((B → (¬A → A)) → A) MP 21,16
23. (¬A → A) → (B → (¬A → A)) LS1
24. ((¬A → A) → ((B → (¬A → A)) → A)) → (((¬A → A) → (B → (¬A → A))) → ((¬A → A) → A)) LS2
25. ((¬A → A) → (B → (¬A → A))) → ((¬A → A) → A) MP 24,22
26. (¬A → A) → A MP 25,23
27. ¬¬A → (¬A → ¬¬A) LS1
28. (¬A → ¬¬A) → (¬A → A) LS3
29. ((¬A → ¬¬A) → (¬A → A)) → (¬¬A → ((¬A → ¬¬A) → (¬A → A))) LS1
30. ¬¬A → ((¬A → ¬¬A) → (¬A → A)) MP 29,28
31. (¬¬A → ((¬A → ¬¬A) → (¬A → A))) → ((¬¬A → (¬A → ¬¬A)) → (¬¬A → (¬A → A))) LS2
32. (¬¬A → (¬A → ¬¬A)) → (¬¬A → (¬A → A)) MP 31,30
33. ¬¬A → (¬A → A) MP 32,27
34. ((¬A → A) → A) → (¬¬A → ((¬A → A) → A)) LS1
35. ¬¬A → ((¬A → A) → A) MP 34,26
36. (¬¬A → ((¬A → A) → A)) → ((¬¬A → (¬A → A)) → (¬¬A → A)) LS2
37. (¬¬A → (¬A → A)) → (¬¬A → A) MP 36,35
38. ¬¬A → A MP 37,33
39. (¬¬A → A) → ((A → B) → (¬¬A → A)) LS1
40. (A → B) → (¬¬A → A) MP 39,38
41. ((A → B) → ((¬¬A → A) → (¬¬A → B))) → (((A → B) → (¬¬A → A)) → ((A → B) → (¬¬A → B))) LS2
42. ((A → B) → (¬¬A → A)) → ((A → B) → (¬¬A → B)) MP 41,7
43. (A → B) → (¬¬A → B) MP 42,40
44. ¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B) LS1
45. (¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))) LS3
46. ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B)))) → (¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))))) LS1
47. ¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B)))) MP 46,45
48. (¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))))) → ((¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B)) → (¬¬B → (¬B → ¬(B → (¬¬B → ¬B))))) LS2
49. (¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B)) → (¬¬B → (¬B → ¬(B → (¬¬B → ¬B)))) MP 48,47
50. ¬¬B → (¬B → ¬(B → (¬¬B → ¬B))) MP 49,44
51. (¬¬B → (¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) LS2
52. (¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B))) MP 51,50
53. (¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B) LS3
54. ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B)) → ((¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B))) LS1
55. (¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B)) MP 54,53
56. ((¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B))) → (((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B))) LS2
57. ((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B)) MP 56,55
58. (¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B) MP 57,52
59. (¬¬B → ¬B) → (B → (¬¬B → ¬B)) LS1
60. ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B)) → (((¬¬B → ¬B) → (B → (¬¬B → ¬B))) → ((¬¬B → ¬B) → ¬B)) LS2
61. ((¬¬B → ¬B) → (B → (¬¬B → ¬B))) → ((¬¬B → ¬B) → ¬B) MP 60,58
62. (¬¬B → ¬B) → ¬B MP 61,59
63. ¬¬¬B → (¬¬B → ¬¬¬B) LS1
64. (¬¬B → ¬¬¬B) → (¬¬B → ¬B) LS3
65. ((¬¬B → ¬¬¬B) → (¬¬B → ¬B)) → (¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B))) LS1
66. ¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B)) MP 65,64
67. (¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B))) → ((¬¬¬B → (¬¬B → ¬¬¬B)) → (¬¬¬B → (¬¬B → ¬B))) LS2
68. (¬¬¬B → (¬¬B → ¬¬¬B)) → (¬¬¬B → (¬¬B → ¬B)) MP 67,66
69. ¬¬¬B → (¬¬B → ¬B) MP 68,63
70. ((¬¬B → ¬B) → ¬B) → (¬¬¬B → ((¬¬B → ¬B) → ¬B)) LS1
71. ¬¬¬B → ((¬¬B → ¬B) → ¬B) MP 70,62
72. (¬¬¬B → ((¬¬B → ¬B) → ¬B)) → ((¬¬¬B → (¬¬B → ¬B)) → (¬¬¬B → ¬B)) LS2
73. (¬¬¬B → (¬¬B → ¬B)) → (¬¬¬B → ¬B) MP 72,71
74. ¬¬¬B → ¬B MP 73,69
75. (¬¬¬B → ¬B) → (B → ¬¬B) LS3
76. B → ¬¬B MP 75,74
77. (B → ¬¬B) → (¬¬A → (B → ¬¬B)) LS1
78. ¬¬A → (B → ¬¬B) MP 77,76
79. (¬¬A → (B → ¬¬B)) → ((¬¬A → B) → (¬¬A → ¬¬B)) LS2
80. (¬¬A → B) → (¬¬A → ¬¬B) MP 79,78
81. ((¬¬A → B) → (¬¬A → ¬¬B)) → ((A → B) → ((¬¬A → B) → (¬¬A → ¬¬B))) LS1
82. (A → B) → ((¬¬A → B) → (¬¬A → ¬¬B)) MP 81,80
83. ((A → B) → ((¬¬A → B) → (¬¬A → ¬¬B))) → (((A → B) → (¬¬A → B)) → ((A → B) → (¬¬A → ¬¬B))) LS2
84. ((A → B) → (¬¬A → B)) → ((A → B) → (¬¬A → ¬¬B)) MP 83,82
85. (A → B) → (¬¬A → ¬¬B) MP 84,43
86. (¬¬A → ¬¬B) → (¬B → ¬A) LS3
87. ((¬¬A → ¬¬B) → (¬B → ¬A)) → ((A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A))) LS1
88. (A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A)) MP 87,86
89. ((A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A))) → (((A → B) → (¬¬A → ¬¬B)) → ((A → B) → (¬B → ¬A))) LS2
90. ((A → B) → (¬¬A → ¬¬B)) → ((A → B) → (¬B → ¬A)) MP 89,88
91. (A → B) → (¬B → ¬A) MP 90,85
```
[Try it online!](https://tio.run/##xVhbbuM2FP3XKlgBhSWUNurkb2ZSQCpQpECKGdTzoSA2PG4tjwXIkmBxkhZpfruAriOryFK6kfRSlGSSIinZkqcIkEiX55z7JE0n26dx@nmcP0SvryuS7py7678@Llw0Hv@A7q4X@PH3dB0uyZ9Z6FzjVZxtV@4TLoAf3YlVMlrwE8t6yBliMakeHRvZb@05sV38kAMiSYkTMB375dkGI87JioS7MCFLWAFItHECfMswwhoF2//@/Y/MugXWtxrWLWO9Gytdce9FjoHLBMqXCQ9gkbN19iwsl/7L1JzCXWkrInBtAR4IwGaaFH7Ai@qCMqdaiSoEQey31Xp5gN5VzYRWSSvBYTIC6HQwv5p@/4RFEJ0KK86nlcvH4ApC8mhcS@y5MDx8VBOAXojQCu3jH10XVwa/ePSoTSFx2ZCgffBcTP/4TMZXebf2YU6W6WYZR0lYZ4Ye4TeaX6FP8@TTE0Y8aNKk2POE9iTbR1DVnISZMyM7gmfw5KI3Y5Rt96s8dA6e6bKL0Yzs4TedqCXdNDmkV5ge9hEJafS7VRZHOXEKA9PDSYy/AWf3qzhaM2cBXrLkWdUxDQc/ctEEGN2N0M1sOlrQvaimXhipFybqpZF6qaDOpN14EEjIdur8Gt6/J1s8Yy2HrYUrs5dAXaGROA6Tz2TrzPCNiwGLohzdfDcdl0yAcRZKagT2ywc0okw8gh9AaPNTBNkQ@zkpmIiaWLowDWm6ccpEpeQxYquwoWYLmEIBS/c49VIZpWVxt9UhcVP0/gvBQTVF8FI@xokDWa/iTbrfhetDWiPYFLKv5eEIoJb7cE/neB@C700Uw/Gelr7sSZRkX8iERKmNP1AuhvMDhjrLwmTtMAvdRfin6I9wXbzT9NmOKKtACdwy@HwzZl4n1uur4yE42ZHvFn@cl@eXZ2apF1xkqc3FK7fkNTQYuQe7golB9hGkAQ2nRrMbMjaG69CT1sLosz@fuqm0muGofVO741fPFYeR4L0aQiOES0KJrIexn4ormgaR5EsxSIjW0PFVUh37JRepLfszKXNlbRmMjnpiGTwpmPZudGNwBA2AxaEpk1dOeh8FXap9ZVXF6B2qdY44y8P42F5rymauyPm9qMpuGh8ZrMBaxwWgqae@ORJS4/IIfjMtjx4Q3NFTFb3@yBEMkiNxk6kQzc/YNoIrBNQqbx2n3biiiIxmuI1D6RSmssaeqpmeoWD8FBjXNUXxmiebMlgpAE@XuBLLh@YJPE99qZId6VeNd03j7dno0hyU33Jn7KRgSMsvK@arPvsrM/ytP//pc@MuqAWW637jKBUYinthX0VXNg/uQCzc4OFb5439IHtU55tl7Vapr@RJmuUOY3ekvlw2vurHdvU4rkTVwqRbgKq8fr3fhlEzlWVIN7ryDZqK9TXyqG9ip86RoeBdqvj/eNa1r31YVTQNyzo1OENPzO1WMIyhnKSmLgI1FEeecLj69TGqYIqfFIKiFK8eyRnFj6gOVFcKuLNL61R/B7ihSqqUNEdwPxVDv3zdyIjJqUsgTl4nnLGkvvp816bVCE/ZtU4sMfxixpsYbitVc869AcNXXIzq7xC@cNOwNCvi9w6/eTsRL9KSk1q9A0r8L71eq@Xfwlqi8V/DptBP8tXyrcdv/c7CRd1fxfDtR9Fm9U3akzqkQ7V2SEs0dkjvzjrNV0uHTOPWiLq/iqJDfOH/Aw "Prolog (SWI) – Try It Online")
A more human-readable version using 5 lemmas:
```
Lemma 1: From A → B and B → C, instantiate A → C. (5 steps)
1. B → C                                         given
2. (B → C) → (A → (B → C))                       L.S.1
3. A → (B → C)                                   M.P. (1,2)
4. (A → (B → C)) → ((A → B) → (A → C))           L.S.2
5. (A → B) → (A → C)                             M.P. (3,4)
6. A → B                                         given
7. A → C                                         M.P. (6,5)
Lemma 2: ¬A → (A → B) (7 steps)
1. ¬A → (¬B → ¬A)                                L.S.1
2. (¬B → ¬A) → (A → B)                           L.S.3
3. ¬A → (A → B)                                  Lemma 1 (1,2)
Lemma 3: From A → (B → C) and A → B, instantiate A → C. (3 steps)
1. A → (B → C)                                   given
2. (A → (B → C)) → ((A → B) → (A → C))           L.S.2
3. (A → B) → (A → C)                             M.P. (1,2)
4. A → B                                         given
5. A → C                                         M.P. (4,3)
Lemma 4: ¬¬A → A (31 steps)
1. ¬A → (A → ¬(B → (¬A → A)))                    Lemma 2
2. (¬A → (A → ¬(B → (¬A → A)))) → 
   ((¬A → A) → (¬A → ¬(B → (¬A → A))))           L.S.2
3. (¬A → A) → (¬A → ¬(B → (¬A → A)))             M.P. (1,2)
4. (¬A → ¬(B → (¬A → A))) →((B → (¬A → A)) → A)  L.S.3
5. (¬A → A) → ((B → (¬A → A)) → A)               Lemma 1 (3,4)
6. (¬A → A) → (B → (¬A → A))                     L.S.1
7. (¬A → A) → A                                  Lemma 3 (5,6)
8. ¬¬A → (¬A → A)                                Lemma 2
9. ¬¬A → A                                       Lemma 1 (8,7)
Lemma 5: (A → B) → (¬¬A → B) (43 steps)
1. (A → B) → (¬¬A → (A → B))                     L.S.1
2. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))     L.S.2
3. (A → B) → ((¬¬A → A) → (¬¬A → B))             Lemma 1 (1,2)
4. ¬¬A → A                                       Lemma 4
5. (¬¬A → A) → ((A → B) → (¬¬A → A))             L.S.1
6. (A → B) → (¬¬A → A)                           M.P. (4,5)
7. (A → B) → (¬¬A → B)                           Lemma 3 (3,6)
Theorem: (A → B) → (¬B → ¬A)
1. (A → B) → (¬¬A → B)                           Lemma 5
2. ¬¬¬B → ¬B                                     Lemma 4
3. (¬¬¬B → ¬B) → (B → ¬¬B)                       L.S.3
4. B → ¬¬B                                       M.P. (2,3)
5. (B → ¬¬B) → (¬¬A → (B → ¬¬B))                 L.S.1
6. ¬¬A → (B → ¬¬B)                               M.P. (4,5)
7. (¬¬A → (B → ¬¬B)) → ((¬¬A → B) → (¬¬A → ¬¬B)) L.S.2
8. (¬¬A → B) → (¬¬A → ¬¬B)                       M.P. (6,7)
9. (A → B) → (¬¬A → ¬¬B)                         Lemma 1 (1,8)
10.(¬¬A → ¬¬B) → (¬B → ¬A)                       L.S.3
11.(A → B) → (¬B → ¬A)                           Lemma 1 (9,10)
```
[Answer]
**59 steps**
Norman Megill, author of Metamath has [told me](https://groups.google.com/d/msg/metamath/4Xaz4dtB_2E/QPZJbs8MDgAJ) about a 59 step proof, which I'm going to post here in this community wiki. The original can be found in theorem 2.16 on this page.
<http://us.metamath.org/mmsolitaire/pmproofs.txt>
Norm says: This page would provide plenty of challenges for you to beat!
Here's the proof
```
((P -> Q) -> (~ Q -> ~ P)); ! *2.16
((P -> Q) -> (~ Q -> ~ P)); ! Result of proof
DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311
; ! 59 steps
```
The proof is in Polish notation, so it starts from the conclusion and
continues backwards until every term has been satisified by an axiom.
The character mapping is as follows: "1" is LS axiom 1, "2" is LS axiom 2, "3"
is LS axiom 3, and "D" is Modus Ponens.
Here's the proof in @W-W's suggested format
```
01 ax-1          $a |- ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) )
02 ax-1          $a |- ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) )
03 ax-3          $a |- ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) )
04 ax-1          $a |- ( ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) )
05 3,4 ax-mp     $a |- ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) )
06 ax-2          $a |- ( ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) → ( ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) )
07 5,6 ax-mp     $a |- ( ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) )
08 2,7 ax-mp     $a |- ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) )
09 ax-3          $a |- ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) )
10 ax-1          $a |- ( ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) → ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) )
11 9,10 ax-mp    $a |- ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) )
12 ax-2          $a |- ( ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) → ( ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) )
13 11,12 ax-mp   $a |- ( ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) )
14 8,13 ax-mp    $a |- ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) )
15 ax-2          $a |- ( ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) → ( ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ¬ B ) ) )
16 14,15 ax-mp   $a |- ( ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ¬ B ) )
17 1,16 ax-mp    $a |- ( ¬ ¬ ¬ B → ¬ B )
18 ax-3          $a |- ( ( ¬ ¬ ¬ B → ¬ B ) → ( B → ¬ ¬ B ) )
19 17,18 ax-mp   $a |- ( B → ¬ ¬ B )
20 ax-1          $a |- ( ( B → ¬ ¬ B ) → ( A → ( B → ¬ ¬ B ) ) )
21 19,20 ax-mp   $a |- ( A → ( B → ¬ ¬ B ) )
22 ax-2          $a |- ( ( A → ( B → ¬ ¬ B ) ) → ( ( A → B ) → ( A → ¬ ¬ B ) ) )
23 21,22 ax-mp   $a |- ( ( A → B ) → ( A → ¬ ¬ B ) )
24 ax-1          $a |- ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) )
25 ax-1          $a |- ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) )
26 ax-3          $a |- ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) )
27 ax-1          $a |- ( ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) )
28 26,27 ax-mp   $a |- ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) )
29 ax-2          $a |- ( ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) → ( ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) ) → ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) )
30 28,29 ax-mp   $a |- ( ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) ) → ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) )
31 25,30 ax-mp   $a |- ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) )
32 ax-3          $a |- ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) )
33 ax-1          $a |- ( ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) → ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) ) )
34 32,33 ax-mp   $a |- ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) )
35 ax-2          $a |- ( ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) ) → ( ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) ) )
36 34,35 ax-mp   $a |- ( ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) )
37 31,36 ax-mp   $a |- ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) )
38 ax-2          $a |- ( ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) )
39 37,38 ax-mp   $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) )
40 ax-2          $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ( ¬ ¬ A → A ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
41 ax-2          $a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ( ¬ ¬ A → A ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) → ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
42 40,41 ax-mp   $a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
43 39,42 ax-mp   $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) )
44 ax-1          $a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
45 43,44 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
46 ax-2          $a |- ( ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) → ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) ) → ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
47 45,46 ax-mp   $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) ) → ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
48 24,47 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) )
49 ax-3          $a |- ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) )
50 ax-1          $a |- ( ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) → ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
51 49,50 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) )
52 ax-2          $a |- ( ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) → ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
53 51,52 ax-mp   $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) )
54 48,53 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) )
55 ax-1          $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) → ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
56 54,55 ax-mp   $a |- ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) )
57 ax-2          $a |- ( ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) → ( ( ( A → B ) → ( A → ¬ ¬ B ) ) → ( ( A → B ) → ( ¬ B → ¬ A ) ) ) )
58 56,57 ax-mp   $a |- ( ( ( A → B ) → ( A → ¬ ¬ B ) ) → ( ( A → B ) → ( ¬ B → ¬ A ) ) )
59 23,58 ax-mp   $a |- ( ( A → B ) → ( ¬ B → ¬ A ) )
```
[Try it online!](https://tio.run/##zVfdbts2FL7XU3ACCksYLczJXdsMkAcMGZCixdwLBbGharNcC5AlwWKTDllu9wB7jj5FH2Uvkh2KkkVKpH4s2S0aJDL5/ZxzeA7lJvs4jD9O04fg@dkj8c64u/77/cpE0@nP6O56hR//jNe@S/5KfOMae2Gy9cwnnAHfm5aWM1rwlqY9pAyxsopHQ0f6K31JdBM/pICIYmI4TEf/@kWHRZwSj/g7PyIu7AAk2BgOvmUYYY@C9f/@@bfKugXWCwXrlrFeT6VW3OcsR8dkAvkHiwewyNk@exa2c/88NSOzy9eyCExdgDsCsJ4mhZd4UV1Q5lQLUYkgiP3hrd0SelccJhxVZccpO8OBk3aWV7OfnrAIol2hhemssHx0riAkm8blYtuE5uGjsgB6IUIL9Bz/Ypq4WJhnjzZdk0hc1iToOdgmpn/mTGYuc9f2fkrceOOGQeQfMkOP8Bstr9CHZfThCSMeZNUp@jKiZ5LsA6hqSvzEWJAdwQt4MtHLKUq2ey/1jdKZbpsYLcgeftOOcunQpJBetvSwD4hPo995SRikxMgWmB6OQvwDmN17YbBmZg52WfKs6piGgx@5aByM7iboZjGbrOgsyqkXjdSLJuplI/VSQl1UprEUiMh2Zvzu378lW7xgRw6jhYtlO4K6wkHi0I8@kq2xwDcmBiwKUnTz42yaMwHGrVBSLbA379CEMvEE/gFCmZ8kyJrYb1HGRHSJpQvdEMcbI0@0kjxGbBcGarGCLhSwdMapS7FY2Ran7RAS10VvPxHsFF0EH/LHMDIgay/cxPudvy7TmsBQVL3c8gqgK/f@nvbx3gfvTRDC9R7nXroVRMknYpEg1vE7ysVwf0BTJ4kfrQ22QqcI/xp89tfZZ5o@m4i8CpTAbYPnyylztbTnZwN9/ZL/zBHc8cgoH7kdE5maHAo/KopUozeJdzrglVHmHid3EQhcRU5vrDiKMxhzp3fmjEWnAQ2oOrbe9f9OYtEG8bk8OsC5Q1DnN6@N4KjKbWM3rlnLqI1s1jxeY2fWMlKD78Butf2G/tqRzIZj6ta83V@58gTbOuYoMU2xI7MQ7nHeqlCqrGUaVRxj2yqVjGU3eDRxizozRNWtfgW24jiU/D1mNzqImOI9IdMrkNXvSs3Yg65dTo0q15E1pVUY20NWxdE9uHqfLg9Rt2dHSGvdtXpn9tR6c4oYG1HiZItR22KPD9NR9/VAXWUvD9VV9e/geJU9e9TN0FaZM/hoPdDSqrZ1TftboR6z@hQ7s3tw6@y6pvrdMbr6gXd85Y6vvOw98M3j0AZrHJ1H1/thvGqfSD2vwKliL3v2yG@GLdVt79Ez@2q9ObUulvAOX99tRde2cnp1abtan67soNajC7vE1qfruk@yugon99F6oNsiauyL@YAqDFAQYj4uhuqZN/2PVpVz@wmPpKp1wmn/Aw "Prolog (SWI) – Try It Online")
Here it is in The Incredible Proof Machine
[![enter image description here](https://i.stack.imgur.com/zpFi0.png)](https://i.stack.imgur.com/zpFi0.png)
[png](https://raw.githubusercontent.com/Antony74/contraposition/master/incredible-proof.png) [svg](https://antony74.github.io/contraposition/incredible-proof.svg)
]