From d652cf6004dc66e4da164280cfe4b05a84dbfb1e Mon Sep 17 00:00:00 2001 From: Felix Linker Date: Fri, 3 Nov 2023 10:54:06 +0100 Subject: [PATCH] Fix figure overflow Currently overflows. Can be seen here: https://tamarin-prover.github.io/manual/master/book/011_advanced-features.html#non-provable-lemmas --- src/011_advanced-features.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/011_advanced-features.md b/src/011_advanced-features.md index 74b933d..b19dd36 100644 --- a/src/011_advanced-features.md +++ b/src/011_advanced-features.md @@ -737,7 +737,7 @@ Tamarins reasoning for subterms works well for irreducible operators. For reduci In the following picture one can see the subterm with the reducible operator `fst` on the right side. Therefore, on the left side, the proof is marked yellow (with the blue line marking the current position). Also, this example demonstrates in `lemma GreenYellow`, that in an `exists-trace` lemma, a trace can be still found and the lemma proven even if there is a part of the proof that cannot be finished. Analogously, `lemma RedYellow` demonstrates that a `all-traces` lemma can still be disproven if a violating trace was found. The last two lemmas are ones where no traces were found in the rest of the proof, thus the overall result of the computation is `Tamarin cannot prove this property`. -![Subterms](../images/YellowSubterms.png "Subterms")\ +![Subterms](../images/YellowSubterms.png "Subterms"){width=100%}\ #### Subterm Store