From cd042d04e665da3c8dd6b2673e5914f8f5686eac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maciej=20Pir=C3=B3g?= <maciej.adam.pirog@gmail.com>
Date: Thu, 8 Oct 2020 22:08:52 +0200
Subject: [PATCH 1/2] Update README.md

---
 README.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index aa2f9e6..3cd6943 100644
--- a/README.md
+++ b/README.md
@@ -149,7 +149,7 @@ As a convention, we write verification logic expressions in curly braces (except
 ```
 (impl (P 0)
       (forall (x) (impl (>= x 0) (P x) (P (+ x 1))))
-	  (forall (x) (impl (>= x 0) (P x))))
+      (forall (x) (impl (>= x 0) (P x))))
 ```
 
 while
@@ -159,7 +159,7 @@ while
 ```
 (impl (forall (x) (impl (>= x 0)
                         (forall (y) (impl (>= y 0) (< y x)
-						                  (P y)))
+                                          (P y)))
                         (P x)))
       (forall (x) (impl (>= x 0) (P x))))
 ```
@@ -238,4 +238,4 @@ Axioms can be defined before the main statement of the program:
   (assert {FACTORIAL n res})))
 ```
 
-```(check f)``` 
+```(check f)``` run Z3 on a goal. As in the case of axioms, the formula ```f``` is closed with a universal quantifier.

From 43d88d9fa8c94d2baba3a92eecbaaa27eaf50418 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maciej=20Pir=C3=B3g?= <maciej.adam.pirog@gmail.com>
Date: Thu, 8 Oct 2020 22:11:48 +0200
Subject: [PATCH 2/2] Update README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 3cd6943..225c1f6 100644
--- a/README.md
+++ b/README.md
@@ -10,7 +10,7 @@ The __grzb__ verifier implements both partial and total correctness rules of the
 
 While programs are written in LISP-y syntax:
 
-<img alt="Emacs in grzb mode" src="https://github.com/maciejpirog/grzb/blob/master/other/screenshot1.png" width="80%">
+<img alt="Emacs in grzb mode" src="https://raw.githubusercontent.com/maciejpirog/grzb/master/other/screenshot1.png" width="90%">
 
 In terminal: