diff --git a/README.md b/README.md
index ef0cf6f..b8b437b 100644
--- a/README.md
+++ b/README.md
@@ -1,10 +1,10 @@
 # tryCoq
 ![Logo](assets/logo.png)
 
-tryCoq provides interactive equational proof with ADT type
+**tryCoq** provides an **interactive equational proof system** for programs defined with **algebraic data types (ADTs)**.
 
-tryCoq is an **interactive proof assistant** that takes **OCaml code** as input and allows users to **perform proofs interactively**.  
-It is designed for reasoning about functional programs using techniques from **structural induction**, **equational reasoning**.
+It is an **interactive proof assistant** that takes **OCaml code** as input and allows users to **perform proofs interactively**.  
+tryCoq is designed for reasoning about functional programs using techniques such as **structural induction** and **equational reasoning**.
 
 ---
 
@@ -25,7 +25,7 @@ Goal (to prove interactively):
 forall (x:nat), add x Z = x
 ```
 
-Interactive Proof Sequences:
+Interactive Proof Sequence:
 ```
 >>> induction x
 >>> simpl
@@ -39,15 +39,15 @@ Interactive Proof Sequences:
 
 ## Getting Started
 ### Requirements
-tryCoq use OCaml package manager(OPAM) and dune
+tryCoq uses the OCaml package manager (OPAM) and dune as its build system.
 
 ### Dependencies
-First, run:
+First, build the project:
 ```bash
 dune build
 ```
 
-To install the dependency, run:
+To install the dependency:
 ```bash
 opam install . --deps-only
 ```
@@ -62,27 +62,27 @@ Enter the definition file path (1/2):
 ---
 
 ## Interactive Proving
-First, insert ocaml code location having ADT type and function definitions
-tryCoq take 2 file paths
+1️⃣ **Provide OCaml code containing ADT and function definitions**
+tryCoq requires two file paths as input:
 ```
 Enter the definition file path (1/2):
 > exam.ml
 ```
 
-Second, choose the proof mode
+2️⃣ **Choose the proof mode**
 ```
 Choose the proof type :
 1) Interactive Mode      2) Auto Mode
 1
 ```
 
-Second, insert conjecture that you want to prove
+3️⃣ **Enter the conjecture to prove**
 ```
 No conjecture
 >>> assert forall (x:nat), add x Z = x
 ```
 
-Now, you can proof interactively with tryCoq
+Now, you can perform an interactive proof with tryCoq:
 ```
 1st goal of : forall (nat1:nat), add (nat1) (0) = nat1
 
@@ -99,18 +99,18 @@ forall (nat1:nat), add (nat1) (0) = nat1
 
 ## Proposition Language
 ```
-<prop>  ::= "forall" <prop>
-          | <expr> "=" <expr>
-          | <prop>* "->" <prop>
+<prop>           ::= "forall" <prop>
+                  | <expr> "=" <expr>
+                  | <prop>* "->" <prop>
 
-<expr>  ::= <fun_name> <expr>*
-          | <constructor> <expr>*
-          | <var>
+<expr>           ::= <fun_name> <expr>*
+                  | <constructor> <expr>*
+                  | <var>
 ```
 
-## Proof Language(tactic)
+## Proof Language(Tactics)
 ```
-tactic           ::=
+<tactic>         ::=
                   | "assert" <prop>
                   | "simpl"
                   | "simpl in" <target_label> 
@@ -123,32 +123,24 @@ tactic           ::=
                   | "discriminate"
 
 <target_label>  ::= <fact_label> | "goal"
-
 <rewrite_label> ::= <fact_label> | <lemma_label>
-
 <loc>           ::= "*" | "1" | "2" | ...
-
 <fact_label>    ::= "IH1" | "Case1" | "Cond1" | ...
-
 <lemma_label>   ::= "lemma1" | ...
-
 <var>           ::= "x" | "y" | ...
-
-```
-
-
-```markdown
-| No. | tactic      | Description                 |
-|------|------------------|----------------------------------|
-| 7    | `assert`        | Establish lemma or theroem |
-| 3    | `simpl`         | Simplify the target.           |
-| 4    | `rewrite IH1`   | Rewrite goal using assumption or lemma.   |
-| 2    | `induction x`   | Perform structural induction on `x`.          |
-| 6    | `case x`        | Split goal into two subgoal x is true and x is false |
-| 1    | `intro`        | Introduced variable or implication condtion into the context .         |
-| 5    | `reflexivity`   | Solve equalities of the form `a=a`               |
-| 8    | `discriminate`   | Solve propostion if assumption leads contradiction |
 ```
+---
 
 
+## Proof Language Description
 
+| No. | Tactic | Description |
+|-----|---------|-------------|
+| 1 | `assert` | Introduce a new lemma or theorem to be proven. |
+| 2 | `simpl` | Simplify the current goal. |
+| 3 | `rewrite IH1` | Rewrite the goal using an assumption or lemma. |
+| 4 | `induction x` | Perform structural induction on variable `x`. |
+| 5 | `case x` | Split the goal into subgoals for different cases of `x`. |
+| 6 | `intro` | Introduce a variable or implication into the context. |
+| 7 | `reflexivity` | Solve goals of the form `a = a`. |
+| 8 | `discriminate` | Solve a goal if an assumption leads to a contradiction. |