diff --git a/README.md b/README.md
index b1c94a4..60fdcb1 100644
--- a/README.md
+++ b/README.md
@@ -1,23 +1,72 @@
 # HOLMS: A HOL Light Library for Modal Systems
 
-(c) Copyright, Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini 2024.
+(c) Copyright, Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini 2024. <br>
+(c) Copyright, Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi 2025.
 
 See the [website](https://holms-lib.github.io/) for a brief overview of our [HOLMS library](https://github.com/HOLMS-lib/HOLMS) for the [HOL Light](https://hol-light.github.io/) theorem prover.
 
-This repository introduces HOLMS (HOL-Light Library for Modal Systems), a new framework within the HOL Light proof assistant, designed for automated theorem proving and countermodel construction in modal logics.
-Building on our prior work focused on Gödel-Löb logic (GL), we generalise our approach to cover a broader range of normal modal systems, starting here with the minimal system K.
-HOLMS provides a flexible mechanism for automating proof search and countermodel generation by leveraging labelled sequent calculi, interactive theorem proving, and formal completeness results.
+This repository presents a second version of HOLMS (HOL-Light Library for Modal Systems), a modular framework designed to implement modal reasoning within the HOL Light proof assistant.  
+
+Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/s10817-023-09677-z), we generalise our approach to formalise modal adequacy proofs for axiomatic calculi, thereby enabling the coverage of a broader range of normal modal systems. If the first version of HOLMS, [presented at Overlay 2024](https://ceur-ws.org/Vol-3904/paper5.pdf), partially parametrised the completeness proof for GL and added the minimal system K, this second version of HOLMS fully generalises our method and, as a demonstration of the flexibility of our methodology, four modal system and their adequacy proofs are now implemented in HOLMS:
+- **K**: the minimal system is developed in `k_completeness.ml`;
+- **K4**: a system properly extended by GL is developed in `k4_completeness.ml`;
+- **GL**: provability logic is developed and fully parametrised in `gl_completeness.ml`;
+- **T**: a system that is not extended by GL or K4, nor is an extension of GL or K4 is developed in `t_completeness.ml`.
+
+HOLMS lays the foundation for a comprehensive tool for modal reasoning in HOL, offering a high level of confidence and full automation by providing the essential mathematical components of principled decision algorithms for modal systems. The automated theorem prover and countermodel constructor for K and GL, already integrated into our library in `k_decid.ml` and `gl_decid.ml`, serve as evidence of the feasibility of this approach merging general purpose proof assistants, enriched sequent calculi, and formalised mathematics.
 
 The top-level file is `make.ml`.
 
-The main theorems are:
-1. `GEN_TRUTH_LEMMA` in file `gen_completeness.ml`.
-2. `K_COMPLETENESS_THM` in file `k_completness.ml`
-3. `GL_COMPLETENESS_THM` in file `gl_completness.ml`
+## Main Theorems
+
+For each normal system $S$, implemented in HOLMS in its file `S_completeness.ml`, we prove the following main theorems:
+- 1. **The Correspondence theorem for S** <br> proves that a certain set of finite frames $C$, distinguished by a certain accessibility relation, **correspond** to $S$ (for each frame in the set if $p$ follows from $S$, then $p$ is valid in such a frame). <br>
+$C= CORR S$ and equivalently $\forall F \in C (S \vdash p \implies F \vDash p) \land \forall F((S \vdash p \implies F \vDash p) \implies F \in C)$ 
+(`CORRS_CORR_S`)
+- 2. **Soundness of S with respect to CORR S**  <br>
+proves that if something is a theorem of $S$ then it is valid in its set of correspondent frames. <br>
+$\forall p (S \vdash p \implies CORR S \vDash p)$
+(`S_CORRS_VALID`)
+- 3. **Consistency of S** <br>
+proves that $S$ cannot prove the false. <br>
+$S \not \vdash \bot$
+(`S_CONSISTENT`)
+- 4. **Completeness of S related to CORR S** <br>
+proves that if someting holds in the set correspondent to $S$, then it is a theorem of $S$. <br>
+$\forall p (CORR S \vDash p \implies S \vdash p)$
+(`S_COMPLETENESS_THM`)
+
+For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`.
+
+Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of $S$ or not (`S_RULE`) and a **fully automated theorem prover and countermodel constructor** for $K$ (`k_completeness.ml`) and $GL$ (`gl_completeness.ml`).
+
+
+To generalise and parametrise the proofs of completeness for normal systems as much as possible, we develop four main theorems in `gen_completeness.ml`:
+1. `GEN_TRUTH_LEMMA`;
+2. `GEN_ACCESSIBILITY_LEMMA`;
+3.  `GEN_COUNTERMODEL_ALT `
+4.  `GEN_LEMMA_FOR_GEN_COMPLETENESS`
+   
 
 # Usage guide and source code
 
-## Axiomatic Definition
+## Axiomatic Calcus 
+We inductively define the **axioms** of our modal calculus (`K_AXIOMS`).
+```
+let KAXIOM_RULES,KAXIOM_INDUCT,KAXIOM_CASES = new_inductive_definition
+  `(!p q. KAXIOM (p --> (q --> p))) /\
+   (!p q r. KAXIOM ((p --> q --> r) --> (p --> q) --> (p --> r))) /\
+   (!p. KAXIOM (((p --> False) --> False) --> p)) /\
+   (!p q. KAXIOM ((p <-> q) --> p --> q)) /\
+   (!p q. KAXIOM ((p <-> q) --> q --> p)) /\
+   (!p q. KAXIOM ((p --> q) --> (q --> p) --> (p <-> q))) /\
+   KAXIOM (True <-> False --> False) /\
+   (!p. KAXIOM (Not p <-> p --> False)) /\
+   (!p q. KAXIOM (p && q <-> (p --> q --> False) --> False)) /\
+   (!p q. KAXIOM (p || q <-> Not(Not p && Not q))) /\
+   (!p q. KAXIOM (Box (p --> q) --> Box p --> Box q))`;;
+```
+Then, we inductively introduce the **rules of inference** of our calculus (`MODPROVES`).
 ```
 let MODPROVES_RULES,MODPROVES_INDUCT,MODPROVES_CASES =
   new_inductive_definition
@@ -34,8 +83,10 @@ MODPROVES_DEDUCTION_LEMMA
 |- !S H p q. [S . H |~ p --> q] <=> [S . p INSERT H |~ q]
 ```
 
-## Relational semantics
-Kripke's Semantics of formulae.
+## Kripke's Semantics of formulae
+
+We define, by induction on the complexity of a formula, that a certain formula $A$ **holds in a certain world $w$ of a certain model $\langle W, R, V\rangle$**. <br>
+$\langle W, R, V\rangle, w \vDash A$
 ```
 let holds =
   let pth = prove
@@ -53,47 +104,73 @@ let holds =
    (holds WR V (p <-> q) w <=> holds WR V p w <=> holds WR V q w) /\
    (holds WR V (Box p) w <=>
     !w'. w' IN FST WR /\ SND WR w w' ==> holds WR V p w')`;;
-
+```
+We say that a formula $p$ **holds in a certain frame** iff it holds for every model in every world  of that frame. <br>
+$\langle W, R\rangle \vDash p \iff \forall V (\forall w \in W (\langle W, R, V\rangle, w \vDash p$))
+```
 let holds_in = new_definition
   `holds_in (W,R) p <=> !V w:W. w IN W ==> holds (W,R) V p w`;;
-
+```
+We say that a formula $p$ is **valid in a class of frames** iff it holds in every frame of this class. <br>
+$L \vDash p \iff \forall \langle W,R \rangle \in L (\langle W,R \rangle \vDash p)$
+```
 let valid = new_definition
   `L |= p <=> !f:(W->bool)#(W->W->bool). f IN L ==> holds_in f p`;;
 ```
-
-## Soundness and consistency of K
-We prove the consistency of K by modus ponens on the converse of `K_FRAME_VALID`.
+The innovative definition of Kripke's model stands on the notion of **modal frame**, namely an ordered pair where the first object is a non-empty set (_domain of the possible worlds_) and the second one is a binary relation on the first set (_accessibility relation_).
 ```
-K_FRAME_VALID
-|- !H p.
-     [{} . H |~ p]
-     ==> (!q. q IN H ==> K_FRAME:(W->bool)#(W->W->bool)->bool |= q)
-         ==> K_FRAME:(W->bool)#(W->W->bool)->bool |= p
-
-K_CONSISTENT
-|- ~ [{} . {} |~ False]
-
-let K_CONSISTENT = prove
- (`~ [{} . {} |~ False]`,
-  REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K_FRAME_VALID)) THEN
-  REWRITE_TAC[NOT_IN_EMPTY] THEN
-  REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM; IN_K_FRAME; NOT_FORALL_THM] THEN
-  MAP_EVERY EXISTS_TAC [`{0}`; `\x:num y:num. F`] THEN
-  REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);;
+let FRAME_DEF = new_definition
+  `FRAME = {(W:W->bool,R:W->W->bool) | ~(W = {}) /\
+                                       (!x y:W. R x y ==> x IN W /\ y IN W)}`;;
+```
+## Theory of Correspondence
+We define the **set of frames correspondent to S**, i.e. the set of all the finite frames such that if p is a theorem of S, then p holds in this frame. <br>
+{ $\langle W,R \rangle \in FINITE-FRAMES| \forall p (S \vdash p \implies \langle W,R \rangle \vDash p)$ }
+```
+let CORR_DEF = new_definition
+  `CORR S = {(W:W->bool,R:W->W->bool) |
+             (((W,R) IN FINITE_FRAME ) /\
+             (!p. [S. {} |~ p] ==> holds_in (W:W->bool,R:W->W->bool) (p)))}`;;
 ```
+For each one of the normal system S developed in HOLMS we prove what set of frames is correspondent to S ($C= CORR S$), i.e. we prove that every frame that is in C is correspondent to S ($\subseteq$: $\forall F \in C(S \vdash p \implies F \vDash p)$ ) and that every frame that is correspondent to S is in C ($\supseteq$: $\forall F((S \vdash p \implies F \vDash p) \implies F \in C)$  ).
 
-## Soundness and consistency of GL
-To develop this proof of consistency we use modal correspondence theory for GL, therefore we prove `TRANSNT_EQ_LOB` and we derive as its consequence`GL_ITF_VALID`.
+### K-Finite Frames 
+We prove that the set of **finite frames** is the one correspondent to **$K$**.
+```
+FINITE_FRAME_CORR_K
+ |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;; 
+```
+### T-Finite Reflexive Frames (RF)
+We prove that the set of **finite reflexive frames** is the one correspondent to **$T$**.
+```
+let RF_DEF = new_definition
+ `RF =
+  {(W:W->bool,R:W->W->bool) |
+   ~(W = {}) /\
+   (!x y:W. R x y ==> x IN W /\ y IN W) /\
+   FINITE W /\
+   (!x. x IN W ==> R x x)}`;;
 
+RF_CORR_T
+ |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;;
 ```
-let TRANSNT_DEF = new_definition
-  `TRANSNT =
-   {(W:W->bool,R:W->W->bool) |
-    ~(W = {}) /\
-    (!x y:W. R x y ==> x IN W /\ y IN W) /\
-    (!x y z:W. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\
-    WF(\x y. R y x)}`;;
+### K4-Finite Transitive Frames (TF)
+We prove that the set of **finite transitive frames** is the one correspondent to **$K4$**.
+```
+let TF_DEF = new_definition
+ `TF =
+  {(W:W->bool,R:W->W->bool) |
+   ~(W = {}) /\
+   (!x y:W. R x y ==> x IN W /\ y IN W) /\
+   FINITE W /\
+   (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;
 
+TF_CORR_K4
+ |-`TF: (W->bool)#(W->W->bool)->bool = CORR K4_AX`;;
+```
+### GL-Finite Irreflexive and Transitive Frames (ITF)
+We prove that the set of **finite transitive and irreflexive frames** is the one correspondent to **$GL$**.
+```
 let ITF_DEF = new_definition
   `ITF =
    {(W:W->bool,R:W->W->bool) |
@@ -103,26 +180,70 @@ let ITF_DEF = new_definition
     (!x. x IN W ==> ~R x x) /\
     (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;
 
-TRANSNT_EQ_LOB
-|- !W R. (!x y:W. R x y ==> x IN W /\ y IN W)
-         ==> ((!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z
-                       ==> R x z) /\
-              WF (\x y. R y x) <=>
-              (!p. holds_in (W,R) (Box(Box p --> p) --> Box p)))
+ITF_CORR_GL
+ |-`ITF: (W->bool)#(W->W->bool)->bool = CORR GL_AX`;;
+```
+
+## Soundness and Consistency
+We parametrically demonstrate the **soundness** of each $S$ with respect to $CORR S$.
+```
+GEN_CORR_VALID
+|- `!S p. [S. {} |~ p] ==> CORR S:(W->bool)#(W->W->bool)->bool |= p`;;
+```
 
-GL_TRANSNT_VALID
-|- !H p. [GL_AX . H |~ p] /\
-         (!q. q IN H ==> TRANSNT:(W->bool)#(W->W->bool)->bool |= q)
-         ==> TRANSNT:(W->bool)#(W->W->bool)->bool |= p
+Then, by specializing the proof of `GEN_CORR_VALID`, we prove the soundness of each normal system  $S$ developed in HOLMS with respect to its correspondent frame.
+Moreover we prove its **consistency**, by modus ponens on the converse of `S_CORRS_VALID`.
 
-GL_ITF_VALID
-|- !p. [GL_AX . {} |~ p] ==> ITF:(W->bool)#(W->W->bool)->bool |= p
+### Soundness and consistency of K
 ```
+let K_FINITE_FRAME_VALID = prove
+(`!p. [{} . {} |~ p] ==> FINITE_FRAME:(W->bool)#(W->W->bool)->bool |= p`,
+ASM_MESON_TAC[GEN_CORR_VALID; FINITE_FRAME_CORR_K]);;
 
-The consistency theorem for GL is proved by modus ponens on the converse of `GL_ITF_VALID`.
+let K_CONSISTENT = prove
+ (`~ [{} . {} |~ False]`,
+  REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K_FINITE_FRAME_VALID)) THEN
+  REWRITE_TAC[NOT_IN_EMPTY] THEN
+  REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM; IN_FINITE_FRAME; NOT_FORALL_THM] THEN
+  MAP_EVERY EXISTS_TAC [`{0}`; `\x:num y:num. F`] THEN
+  REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);;
+```
+
+### Soundness and consistency of T
+```
+let T_RF_VALID = prove
+ (`!p. [T_AX . {} |~ p] ==> RF:(W->bool)#(W->W->bool)->bool |= p`,
+  MESON_TAC[GEN_CORR_VALID; RF_CORR_T]);;
+
+let T_CONSISTENT = prove
+ (`~ [T_AX . {} |~  False]`,
+  REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] T_RF_VALID)) THEN
+  REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM;
+              IN_RF; NOT_FORALL_THM] THEN
+  MAP_EVERY EXISTS_TAC [`{0}`; `\x:num y:num. x = 0 /\ x = y`] THEN
+  REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);;
+```
+
+### Soundness and consistency of K4
+```
+let K4_TF_VALID = prove
+ (`!p. [K4_AX . {} |~ p] ==> TF:(W->bool)#(W->W->bool)->bool |= p`,
+  MESON_TAC[GEN_CORR_VALID; TF_CORR_K4]);;
+
+let K4_CONSISTENT = prove
+ (`~ [K4_AX . {} |~  False]`,
+  REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K4_TF_VALID)) THEN
+  REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM;
+              IN_TF; NOT_FORALL_THM] THEN
+  MAP_EVERY EXISTS_TAC [`{0}`; `\x:num y:num. F`] THEN
+  REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);;
+```
+
+### Soundness and consistency of GL
 ```
-GL_consistent
-|- ~ [GL_AX . {} |~  False]
+let GL_ITF_VALID = prove
+(`!p. [GL_AX . {} |~ p] ==> ITF:(W->bool)#(W->W->bool)->bool |= p`,
+ASM_MESON_TAC[GEN_CORR_VALID; ITF_CORR_GL]);;
 
 let GL_consistent = prove
  (`~ [GL_AX . {} |~  False]`,
@@ -133,97 +254,179 @@ let GL_consistent = prove
   REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);;
 ```
 
-## Completeness theorems
+## Completeness Theorems
+We first sketch the idea behind the demonstration and, then, we will present a three-step proof.
 
-The proof is organized in three steps.
-We can observe that, by working with HOL, it is possible to identify all those lines of reasoning that are _parametric_ for P (the specific propriety of each frame of a logic) and S (the set of axioms of the logic)
-and develop each of of the three steps while avoiding code duplication as much as possible.
-In particular  the step 3 is already fully formalised in HOLMS with the `GEN_TRUTH_LEMMA`.
+### The Idea behind the Proof
 
-### STEP 1
-Identification of a model <W,R,V> depending on a formula p and, in particular, of a non-empty set of possible worlds given by a subclass of maximal consistent sets of formulas.
+Given a modal system $S$, we want to prove that it is **complete with respect to the set of its correspondent frames**: $\forall p (CORRS \vDash p \implies S \vdash p)$
 
-Parametric Definitions in `gen_completness.ml` (parameters P, S)
 ```
-let FRAME_DEF = new_definition
-  `FRAME = {(W:W->bool,R:W->W->bool) | ~(W = {}) /\
-                                       (!x y:W. R x y ==> x IN W /\ y IN W)}`;;
+S_COMPLETENESS_THM
+|. `!p. ( CORR S |= p ==> [S. {} |~ p])`
+```
+- **1. Rewriting `S_COMPLETENESS`'s statment** <br>
+By using some tautologies and rewritings, we can show that the completeness theorem is equivalent to a more handy sentence:  <br>
+$\forall p (S \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in CORR_S (\exists V_{S,p} \exists m_{S,p} \in W_{S,p} (\langle W_{S,p}, R_{S,p}, V_{S,p} \rangle, m_{S,p} \not \vDash p))$ <br> <br>
+  - A. We rewrote the sentence by _contraposition_. <br>
+   `e GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM];;` <br> <br>
+  - B. We rewrote validity in a set of frames (`valid`) as validity in a certain world of a certain model (`holds`) and we exploited some _propositional tautologies_. <br>
+   `e (REWRITE_TAC[valid; NOT_FORALL_THM; FORALL_PAIR_THM; holds_in; NOT_IMP]);;` <br>
+```
+S_COMPLETENESS_THM'
+|- `!p. ( `~[S . {} |~ p] ==>
+          (? W R. W,R IN CORR S /\
+            (? V m. m IN W /\
+              ~holds (W,R) V p w)))`
+```
+To prove this rewritten statment, we need to construct a **_countermodel_** $𝓜_{S,p}$ and a "**_counterworld_**" $m_{S,p}$ in the domain of the countermodel for each modal formula $p$. <br> <br>
+We can observe that, by working with HOL, we identify all those lines of reasoning that are **_parametric_** with respect to $S$ (the axiom system) and to  $p$ (the formula we are analysing) and we develop the completeness proof while **avoiding code duplication as much as possible**. <br>
+<br>
+- **2. Reducing a model theoretic-notion to a set/list-theoretic concept** <br>
+The canonical proof of completeness, illustrated in classical textbooks like [George Boolos's "The Logic of Provability"](https://www.cambridge.org/core/books/logic-of-provability/F1549530F91505462083CE2FEB6444AA), exploits the idea of working in a context (_countermodel_) such that: $\forall w \in W_{S,p} (w \in p \iff 𝓜_{S,p},w \vDash p) $. <br> <br>
+Observe that, in such a context, the members of the domain $W_{S,p}$ are set (list in HOLMS) of modal formulas.
+If we are able to construct a countermodel with this constraints, we will easily construct a counterworld $m_{S,p}$ that is a set of formulas not including p.
+<br> <br>
+Then our subgoal would be to prove: <br> 
+```
+S_COMPLETENESS_THM''
+|- `!p. ( `~[S . {} |~ p] ==>
+          (? W R. W,R IN CORR S /\
+            (? M. M IN W /\
+              ~ MEM p M)))`
+```
+This subgoal is much more manageable than the previous one, indeed it reduces the **model-theoretic** notion of _validity_ (`holds (W,R) V p w`) to the **set-theoretic** concept (**list-theoretic** in HOLMS) of _membership_ (`MEM p w`).
+
+
+- **3. What do we need to prove?** <br>
+Given our aim of proving $\forall p(S \not \vdash p \implies \exists \langle W,R \rangle_{S,p} \in CORR S(\exists m_{S,p} \in W_{S,p}(p \not \in m_{S,p})))$, we need a countermodel and counterworld following these constraints: <br> <br>
+  - A. The Kripke's frame $\langle W,R \rangle_{S,p}$ must be **correspondent** to S. <br>
+    $\langle W,R \rangle_{S,p} \in CORRS$ <br> <br>
+  - B. The Kripke's model $𝓜_{S,p} = \langle W,R,V \rangle_{S,p}$ must allows us to **reduce validity to membership**. <br>
+    Namely, for our model $𝓜_{S,p}$ holds $\forall w \in W_{S,p} (w \in p \iff 𝓜_{S,p},w \vDash p) $. <br> <br>
+  - C. The counterworld $m_{S,p}$ must not contain p. <br>
+      $p \not \in m_{S,p}$ <br> <br>
+  - D. $W_{S,p}$ must be a **set of formulas' lists** <br>
+   `CORRS:(form list->bool)#(form list->form list->bool)->bool`. 
+
+
+### STEP 1: Partial definition of a parametric Standard Model 
+
+We partially identify the countermodel $𝓜_{S,p} = \langle W,R,V \rangle_{S,p}$ by defining $W_{S,p}$ as a set of maximal consistent lists, $V$ as a particular binary relation over formulas' atoms and worlds and by requesting two constraints for $R_{S,p}$. The definition of `S_STANDARD_MODEL` in step 1 is fully parametric and does not involve any peculiarities of the modal system $S$.
+
+### Consistency and Maximal Consistency
+Before we build up the countermodel, we define in `consistent.ml` some properties that hold for formulas' lists and that will be usefull to define the domain of the countermodel.
+
+#### Consistent $S$ 
+A list of formulas $X$ is consistent to a set of axioms $S$ iff and only if $S \not \vdash \neg \bigwedge X$
+```
+let CONSISTENT = new_definition
+  `CONSISTENT S (X:form list) <=> ~[S . {} |~ Not (CONJLIST X)]`;;
+```
+
+#### Maximal Consistent $S,p$ <br>
+A list of formulas $X$ is maximal-consistent to a set of axioms $S$ and modal formula $p$ iff $X \ has \ no \ repetitions$, $X \ is \ consistent_S$ and $\forall q (q \ subformula \ p \implies q \in X \lor \neg q \in l)$.
+```
+let MAXIMAL_CONSISTENT = new_definition
+  `MAXIMAL_CONSISTENT S p X <=>
+   CONSISTENT S X /\ NOREPETITION X /\
+   (!q. q SUBFORMULA p ==> MEM q X \/ MEM (Not q) X)`;;
+```
+
+#### Lemma of Extension of Maximal Consistent lists
+$X \ Consistent_S \implies \exists M (X \subseteq M \ \land \ M \ Maximal-Consistent_{S,p} )$
+```
+EXTEND_MAXIMAL_CONSISTENT 
+|- (`!S p X. CONSISTENT S X /\
+           (!q. MEM q X ==> q SUBSENTENCE p)
+           ==> ?M. MAXIMAL_CONSISTENT S p M /\
+                   (!q. MEM q M ==> q SUBSENTENCE p) /\
+                   X SUBLIST M`
+```
+
+### Definition of the parametric Countermodel
+We define a **standard model** such that:
 
+- **A: The Domain $W_{S,p}$  is { $X | Maximal-Consistent_{S,p} \ X$ }** <br> <br>
+As requested, the domain is a set of lists of formulas and, in particular, it is a **subclass of maximal consistent sets of formulas**. <br>
+  Observe that, in principle, we can employ general **sets** of formulas in the formalisation. However, from the practical viewpoint, **lists without repetitions** are better suited in HOL since they are automatically finite and we can easily manipulate them by structural recursion. <br> <br>
+We prove, as requested for the domain of a frame, that $W_{S,p}$ is **non-empty** by using `NONEMPTY_MAXIMAL_CONSISTENT`, a corollary of the lemma of extension of maximal consistent lists.
+```
+NONEMPTY_MAXIMAL_CONSISTENT
+|- `!S p. ~ [S . {} |~ p]
+         ==> ?M. MAXIMAL_CONSISTENT S p M /\
+                 MEM (Not p) M /\
+                 (!q. MEM q M ==> q SUBSENTENCE p)`
+```
+
+- **B: The Accessibility Relation $R_{S,p}$** should meet two conditions
+   - R1: $\forall q \in Form_{\Box} (\Box q \ subformula \ p \implies \forall w \in W_{S,p}(\Box q \in w \iff \forall x (wRx \implies q \in x)))$. <br>
+     This condition ensures that my list-theoretic translation follows kripke's semantics.
+   - R2: $\langle W,R \rangle_{S,p} \in CORR S$. <br>
+    This second condition guarantees one of the four initial constraints.
+
+- **C: The Evaluation Relation $V_{S,p}$** is defined as follows <br>
+  $\forall m \in W_{S,p} \ \forall a \in Atom-Form_{\Box} (mVa \iff a \ subformula \ p \land a \in m)$
+
+
+In particular, in HOLMS's `gen_completeness.ml` we develop a parametric (to $S$ and $p$) definition  of `GEN_STANDARD_FRAME` and `GEN_STANDARD_MODEL` and then we specialize these definitions for each normal system. 
+
+```
 let GEN_STANDARD_FRAME_DEF = new_definition
-  `GEN_STANDARD_FRAME P S p =
-   FRAME INTER P INTER
+  `GEN_STANDARD_FRAME S p =
+   CORR S INTER
    {(W,R) | W = {w | MAXIMAL_CONSISTENT S p w /\
             (!q. MEM q w ==> q SUBSENTENCE p)} /\
             (!q w. Box q SUBFORMULA p /\ w IN W
                    ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))}`;;
 
 let GEN_STANDARD_MODEL_DEF = new_definition
-  `GEN_STANDARD_MODEL P S p (W,R) V <=>
-   (W,R) IN GEN_STANDARD_FRAME P S p /\
+  `GEN_STANDARD_MODEL S p (W,R) V <=>
+   (W,R) IN GEN_STANDARD_FRAME S p /\
    (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`;;
 ```
+Because the definitions of `K_STANDARD_MODEL`, `T_STANDARD_MODEL`, `K4_STANDARD_MODEL` and `GL_STANDARD_MODEL` are just instances of `GEN_STANDARD_FRAME` and `GEN_STANDARD_MODEL` with the parameters `{}`, `T_AX`, `K4_AX` and `GL_AX`, here we present only the definitions for $K4$.
 
-Definitions in `k_completness.ml` (P=K_FRAME, S={})
+Definitions in `k4_completeness.ml` (`S`=`K4_AX`)
 ```
-let K_FRAME_DEF = new_definition
-  `K_FRAME = {(W:W->bool,R) | (W,R) IN FRAME /\ FINITE W}`;;
-
-let K_STANDARD_FRAME_DEF = new_definition
-  `K_STANDARD_FRAME = GEN_STANDARD_FRAME K_FRAME {}`;;
-
-IN_K_STANDARD_FRAME
-|- (W,R) IN K_STANDARD_FRAME p <=>
-   W = {w | MAXIMAL_CONSISTENT {} p w /\
-            (!q. MEM q w ==> q SUBSENTENCE p)} /\
-   (W,R) IN K_FRAME /\
-   (!q w. Box q SUBFORMULA p /\ w IN W
-          ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))
+let K4_STANDARD_FRAME_DEF = new_definition
+`K4_STANDARD_FRAME p = GEN_STANDARD_FRAME K4_AX p`;;  
 
-let K_STANDARD_MODEL_DEF = new_definition
-   `K_STANDARD_MODEL = GEN_STANDARD_MODEL K_FRAME {}`;;
+IN_K4_STANDARD_FRAME
+|- (`!p W R. (W,R) IN K4_STANDARD_FRAME p <=>
+          W = {w | MAXIMAL_CONSISTENT K4_AX p w /\
+                   (!q. MEM q w ==> q SUBSENTENCE p)} /\
+          (W,R) IN TF /\
+          (!q w. Box q SUBFORMULA p /\ w IN W
+                 ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))`
 
-K_STANDARD_MODEL_CAR
-|- K_STANDARD_MODEL p (W,R) V <=>
-   (W,R) IN K_STANDARD_FRAME p /\
-   (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))
-```
+let K4_STANDARD_MODEL_DEF = new_definition
+   `K4_STANDARD_MODEL = GEN_STANDARD_MODEL K4_AX`;;
 
-Definitions in `gl_completness.ml` (P=ITF, S=GL_AX)
+K4_STANDARD_MODEL_CAR
+|- (`!W R p V.
+     K4_STANDARD_MODEL p (W,R) V <=>
+     (W,R) IN K4_STANDARD_FRAME p /\
+     (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`,
 ```
-let ITF_DEF = new_definition
-  `ITF =
-   {(W:W->bool,R:W->W->bool) |
-    ~(W = {}) /\
-    (!x y:W. R x y ==> x IN W /\ y IN W) /\
-    FINITE W /\
-    (!x. x IN W ==> ~R x x) /\
-    (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;
 
-let GL_STANDARD_FRAME_DEF = new_definition
-  `GL_STANDARD_FRAME p = GEN_STANDARD_FRAME ITF GL_AX p`;;
 
-IN_GL_STANDARD_FRAME
-|- !p W R. (W,R) IN GL_STANDARD_FRAME p <=>
-           W = {w | MAXIMAL_CONSISTENT GL_AX p w /\
-                    (!q. MEM q w ==> q SUBSENTENCE p)} /\
-           (W,R) IN ITF /\
-           (!q w. Box q SUBFORMULA p /\ w IN W
-                  ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))
+### STEP 2: Definition of a standard accessibility relation for each S
+The definition of a _standard acessibility relation_ cannot be fully parametrised, at least following the approach presented in classical textbook.
 
-let GL_STANDARD_MODEL_DEF = new_definition
-  `GL_STANDARD_MODEL = GEN_STANDARD_MODEL ITF GL_AX`;;
+Consequently, to avoid code repetions, we will:
 
-GL_STANDARD_MODEL_CAR
-|- !W R p V.
-     GL_STANDARD_MODEL p (W,R) V <=>
-     (W,R) IN GL_STANDARD_FRAME p /\
-     (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))
-```
-
-### STEP 2
-Definition of a “standard” accessibility relation depending on axiom set S between these worlds such that the frame is appropriate to S.
+- A: Define a parametric `GEN_STANDARD_REL` in `gen_completeness.ml`, 
+- B: Complete the definition of `S_STANDARD_REL` in its spefic file `S_completeness.ml`, in a way that guarantees that conditions R1 and R2 holds.
+  In particular we will show:
+  - The most difficult verse of R1's implication in `S_ACCESSIBILITY_LEMMA` <br>
+$\forall q \in Form_{\Box} (\Box q \ subformula \ p \implies \forall w \in W_{S,p}(\Box q \in w \Longleftarrow \forall x (wRx \implies q \in x)))$
+  -   R2 holds for $\langle W_{S,p},$ _S_STANDARD_REL_ $\rangle$ in ` S_MAXIMAL_CONSISTENT`. <br>
+    $\langle W_{S,p},$ _S_STANDARD_REL_ $\rangle  \in CORRS$
+    
+Then `CORRS_IN_STANDARD_S_FRAME` follows as corollary and, given the hypotesis $S \not \vdash p$,  $\langle W_{S,p},$ S_STANDARD_REL $, V_{S,p} \rangle$ is an `S_STANDARD_MODEL`.
 
-Parametric definition of the standard relation in `gen_completness.ml` (parameter S)
+#### A: Parametric definition of the standard relation in `gen_completeness`.
 ```
 let GEN_STANDARD_REL = new_definition
   `GEN_STANDARD_REL S p w x <=>
@@ -232,27 +435,161 @@ let GEN_STANDARD_REL = new_definition
    (!B. MEM (Box B) w ==> MEM B x)`;;
 ```
 
-Definitions in `k_completness.ml` (S={}) and proof of the Accessibility Lemma for K.
+#### B: Definition of the standard relation for K in `k_completeness.ml`.
 ```
 let K_STANDARD_REL_DEF = new_definition
   `K_STANDARD_REL p = GEN_STANDARD_REL {} p`;;
 
 K_STANDARD_REL_CAR
-|- K_STANDARD_REL p w x <=>
+|- `K_STANDARD_REL p w x <=>
    MAXIMAL_CONSISTENT {} p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\
    MAXIMAL_CONSISTENT {} p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\
-   (!B. MEM (Box B) w ==> MEM B x)
-
-K_ACCESSIBILITY_LEMMA_1
-|- !p w q. ~ [{} . {} |~ p] /\
-           MAXIMAL_CONSISTENT {} p w /\
-           (!q. MEM q w ==> q SUBSENTENCE p) /\
-           Box q SUBFORMULA p /\
-           (!x. K_STANDARD_REL p w x ==> MEM q x)
-           ==> MEM (Box q) w
-```
-
-Definitions in `gl_completness.ml` (S=GL_AX) and proofs of the Accessibility Lemma for GL.
+   (!B. MEM (Box B) w ==> MEM B x)`
+```
+
+**Accessibility lemma for K** that ensures the most difficult verse of R1's implication.
+```
+K_ACCESSIBILITY_LEMMA
+|- `!p w q. ~ [{} . {} |~ p] /\
+         MAXIMAL_CONSISTENT {} p w /\
+         (!q. MEM q w ==> q SUBSENTENCE p) /\
+         Box q SUBFORMULA p /\
+         (!x. K_STANDARD_REL p w x ==> MEM q x)
+         ==> MEM (Box q) w`
+```
+**Maximal consistent lemma for K** ensures R2.
+```
+K_MAXIMAL_CONSISTENT
+|- (`!p. ~ [{} . {} |~ p]
+     ==> ({M | MAXIMAL_CONSISTENT {} p M /\
+          (!q. MEM q M ==> q SUBSENTENCE p)},
+          K_STANDARD_REL p) IN FINITE_FRAME`,
+```
+Proof of the corollary that ensures that **our construction for K is a standard frame**.
+```
+g `!p. ~ [{} . {} |~ p]
+       ==> ({M | MAXIMAL_CONSISTENT {} p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, 
+             K_STANDARD_REL p) IN K_STANDARD_FRAME p`;;
+e (INTRO_TAC "!p; not_theor_p");;
+e (REWRITE_TAC [IN_K_STANDARD_FRAME]);;
+e CONJ_TAC;;
+e (MATCH_MP_TAC K_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (INTRO_TAC "!q w; subform w_in");;
+e EQ_TAC;;
+ e (ASM_MESON_TAC[K_STANDARD_REL_CAR]);;
+ e (INTRO_TAC "Implies_Mem_q");;
+   e (HYP_TAC "w_in" (REWRITE_RULE[IN_ELIM_THM]));;
+   e (MATCH_MP_TAC K_ACCESSIBILITY_LEMMA);;
+   e (EXISTS_TAC `p:form`);;
+   e (ASM_REWRITE_TAC[]);;
+let KF_IN_STANDARD_K_FRAME = top_thm();;
+```
+
+
+#### B: Definition of the standard relation for T in `t_completeness.ml`.
+```
+let T_STANDARD_REL_DEF = new_definition
+  `T_STANDARD_REL p w x <=>
+   GEN_STANDARD_REL T_AX p w x`;;
+
+T_STANDARD_REL_CAR
+|- `!p w x.
+     T_STANDARD_REL p w x <=>
+     MAXIMAL_CONSISTENT T_AX p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\
+     MAXIMAL_CONSISTENT T_AX p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\
+     (!B. MEM (Box B) w ==> MEM B x)`
+```
+
+**Accessibility lemma for T** that ensures the most difficult verse of R1's implication.
+```
+T_ACCESSIBILITY_LEMMA
+|- `!p w q.
+   ~ [T_AX . {} |~ p] /\
+   MAXIMAL_CONSISTENT T_AX p w /\
+   (!q. MEM q w ==> q SUBSENTENCE p) /\
+   Box q SUBFORMULA p /\
+   (!x. T_STANDARD_REL p w x ==> MEM q x)
+     ==> MEM (Box q) w`
+```
+**Maximal consistent lemma for T** that ensures R2.
+```
+RF_MAXIMAL_CONSISTENT
+|- `!p. ~ [T_AX . {} |~ p]
+         ==> ({M | MAXIMAL_CONSISTENT T_AX p M /\
+                       (!q. MEM q M ==> q SUBSENTENCE p)},
+                   T_STANDARD_REL p) IN RF `
+```
+Proof of the corollary that ensures that **our construction for T is a standard frame**.
+```
+g `!p. ~ [T_AX . {} |~ p]
+       ==> ({M | MAXIMAL_CONSISTENT T_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, 
+             T_STANDARD_REL p) IN T_STANDARD_FRAME p`;;
+e (INTRO_TAC "!p; not_theor_p");;
+e (REWRITE_TAC [IN_T_STANDARD_FRAME]);;
+e CONJ_TAC;;
+e (MATCH_MP_TAC RF_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
+e (INTRO_TAC "!q w; boxq maxw subw");;
+e EQ_TAC;;
+ e (ASM_MESON_TAC[T_STANDARD_REL_CAR]);;
+ e (ASM_MESON_TAC[T_ACCESSIBILITY_LEMMA]);;
+let RF_IN_T_STANDARD_FRAME = top_thm();;
+```
+#### B: Definition of the standard relation for K4 in `k4_completeness.ml`.
+```
+let K4_STANDARD_REL_DEF = new_definition
+  `K4_STANDARD_REL p w x <=>
+   GEN_STANDARD_REL K4_AX p w x /\
+   (!B. MEM (Box B) w ==> MEM (Box B) x)`;;
+
+K4_STANDARD_REL_CAR
+|- `!p w x.
+     K4_STANDARD_REL p w x <=>
+     MAXIMAL_CONSISTENT K4_AX p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\
+     MAXIMAL_CONSISTENT K4_AX p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\
+     (!B. MEM (Box B) w ==> MEM (Box B) x /\ MEM B x)`
+```
+
+**Accessibility lemma for K4** that ensures the most difficult verse of R1's implication.
+```
+K4_ACCESSIBILITY_LEMMA
+|- `!p w q.
+    ~ [K4_AX . {} |~ p] /\
+    MAXIMAL_CONSISTENT K4_AX p w /\
+    (!q. MEM q w ==> q SUBSENTENCE p) /\
+    Box q SUBFORMULA p /\
+    (!x. K4_STANDARD_REL p w x ==> MEM q x)
+      ==> MEM (Box q) w`
+```
+**Maximal consistent lemma for K4** that ensures R2.
+```
+TF_MAXIMAL_CONSISTENT
+|- `!p. ~ [T_AX . {} |~ p]
+         ==> ({M | MAXIMAL_CONSISTENT T_AX p M /\
+                       (!q. MEM q M ==> q SUBSENTENCE p)},
+                   T_STANDARD_REL p) IN RF `
+```
+Proof of the corollary that ensures that **our construction for K4 is a standard frame**.
+```
+g `!p. ~ [K4_AX . {} |~ p]
+       ==> ({M | MAXIMAL_CONSISTENT K4_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, 
+             K4_STANDARD_REL p) IN K4_STANDARD_FRAME p`;;
+e (INTRO_TAC "!p; not_theor_p");;
+e (REWRITE_TAC [IN_K4_STANDARD_FRAME]);;
+e CONJ_TAC;;
+e (MATCH_MP_TAC TF_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
+e (INTRO_TAC "!q w; boxq maxw subw");;
+e EQ_TAC;;
+ e (ASM_MESON_TAC[K4_STANDARD_REL_CAR]);;
+ e (ASM_MESON_TAC[K4_ACCESSIBILITY_LEMMA]);;
+let K4F_IN_K4_STANDARD_FRAME = top_thm();;
+```
+
+#### B: Definition of the standard relation for GL in `gl_completeness.ml`.
 ```
 let GL_STANDARD_REL_DEF = new_definition
   `GL_STANDARD_REL p w x <=>
@@ -260,79 +597,224 @@ let GL_STANDARD_REL_DEF = new_definition
    (!B. MEM (Box B) w ==> MEM (Box B) x) /\
    (?E. MEM (Box E) x /\ MEM (Not (Box E)) w)`;;
 
+GL_STANDARD_REL_CAR
+|- `!p w x.
+     GL_STANDARD_REL p w x <=>
+     MAXIMAL_CONSISTENT GL_AX p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\
+     MAXIMAL_CONSISTENT GL_AX p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\
+     (!B. MEM (Box B) w ==> MEM (Box B) x /\ MEM B x) /\
+     (?E. MEM (Box E) x /\ MEM (Not (Box E)) w)`
+```
+
+**Accessibility Lemma for GL** that ensures the most difficult verse of R1's implication.
+```
 GL_ACCESSIBILITY_LEMMA
-|- !p M w q.
+|- `!p w q.
      ~ [GL_AX . {} |~ p] /\
-     MAXIMAL_CONSISTENT GL_AX p M /\
-     (!q. MEM q M ==> q SUBSENTENCE p) /\
      MAXIMAL_CONSISTENT GL_AX p w /\
      (!q. MEM q w ==> q SUBSENTENCE p) /\
-     MEM (Not p) M /\
      Box q SUBFORMULA p /\
      (!x. GL_STANDARD_REL p w x ==> MEM q x)
-     ==> MEM (Box q) w
+     ==> MEM (Box q) w`
 ```
-
-### STEP 3
-The reduction of the notion of forcing `holds (W,R) V q w` to that of a set-theoretic (list-theoretic) membership MEM q w
-for every subformula q of p, through a specific atomic evaluation function on (W,R).
-
-Parametric truth lemma in `gen_completness.ml` (parameters P, S)
+**Maximal Consistent Lemma for GL** that ensures R2.
 ```
-GEN_TRUTH_LEMMA
-|- !P S W R p V q.
-     ~ [S . {} |~ p] /\
-     GEN_STANDARD_MODEL P S p (W,R) V /\
-     q SUBFORMULA p
-     ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)
+ITF_MAXIMAL_CONSISTENT
+|- `!p. ~ [GL_AX . {} |~ p]
+         ==> ({M | MAXIMAL_CONSISTENT GL_AX p M /\
+                       (!q. MEM q M ==> q SUBSENTENCE p)},
+                   GL_STANDARD_REL p) IN ITF `
 ```
-
-Truth lemma specified for K in `k_completness.ml` (P=K_FRAME, S={})
+Proof of the corollary that ensures that **our construction for GL is a standard frame**.
 ```
-let K_TRUTH_LEMMA = prove
- (`!W R p V q.
-     ~ [{} . {} |~ p] /\
-     K_STANDARD_MODEL p (W,R) V /\
-     q SUBFORMULA p
-     ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`,
-  REWRITE_TAC[K_STANDARD_MODEL_DEF] THEN MESON_TAC[GEN_TRUTH_LEMMA]);;
+g `!p. ~ [GL_AX . {} |~ p]
+       ==> ({M | MAXIMAL_CONSISTENT GL_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, 
+             GL_STANDARD_REL p) IN GL_STANDARD_FRAME p`;;
+e (INTRO_TAC "!p; not_theor_p");;
+e (REWRITE_TAC [IN_GL_STANDARD_FRAME]);;
+e CONJ_TAC;;
+e (MATCH_MP_TAC ITF_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
+e (INTRO_TAC "!q w; subform max_cons_w implies_w");;
+e EQ_TAC;;
+ e (ASM_MESON_TAC[GL_STANDARD_REL_CAR]);;
+ e (ASM_MESON_TAC[GL_ACCESSIBILITY_LEMMA]);;
+let GLF_IN_GL_STANDARD_FRAME = top_thm();;
 ```
 
-Truth lemma specified for GL in `gl_completness.ml` (P=ITF, S=GL_AX)
+
+### STEP 3: Proving the truth lemma
+In this step we prove that, given a standard model and $S \not \vdash p$, the _desiderandum_ in the proof sketch holds, and indeed something stronger holds:
+_For every subformula q of p_ we can reduce the notion of `holds (W,R) V q w` to the list-theoretic one of membership `MEM q w`.
+
+Observe that we prove this foundamental lemma in a fully parametric way and, moreover, the proof of completeness does not need to specify this lemma for the normal system in analysis. 
+
+#### Parametric truth lemma in `gen_completeness.ml` (parameters P, S)
 ```
-let GL_truth_lemma = prove
- (`!W R p V q.
-     ~ [GL_AX . {} |~ p] /\
-     GL_STANDARD_MODEL p (W,R) V /\
+GEN_TRUTH_LEMMA
+|- `!S W R p V q.
+     ~ [S . {} |~ p] /\
+     GEN_STANDARD_MODEL S p (W,R) V /\
      q SUBFORMULA p
-     ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`,
-  REWRITE_TAC[GL_STANDARD_MODEL_DEF] THEN MESON_TAC[GEN_TRUTH_LEMMA]);;
+     ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`
 ```
 
 ### The Theorems
 
-Completeness of K in `k_completness.ml`.
-This proof uses the `K_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completness theorem for K is completely parametrized.
-```
-K_COMPLETENESS_THM
-|- !p. K_FRAME:(form list->bool)#(form list->form list->bool)->bool |= p
-       ==> [{} . {} |~ p]
+We built up a _countermodel_ $\langle W,R,V \rangle_{S,p}$ that is a _standard model for S_, and now we want to prove that a _counterworld_ in this model exists:  $\exists m_{S,p} \in W_{S,p} (p \not \in m_{S,p} )$. So we need an $m_{S,p}$ such that:
+ - A: $m_{S,p} \in W_{S,p}$ that is to say $Maximal-Consistent_{S,p} \ m$;
+ - B: $p \not \in m_{S,p}$
+
+Thanks to our theorem `NONEMPTY_MAXIMAL_CONSISTENT` $\forall p (S \vdash p \implies (\exists m (Maximal-Consistent_{S,p} \ m \ \land \ \neg p \in M))$, we know that such an $m_{S,p}$ exists and we can prove `GEN_COUNTERMODEL_ALT`. Observe, indeed, that $Maximal-Consistent_{S,p} \ m \ \land \ \neg p \in m_{S,p} \implies p \not \in m_{S,p}$.
+```
+NONEMPTY_MAXIMAL_CONSISTENT
+|- `!S p. ~ [S . {} |~ p]
+         ==> ?M. MAXIMAL_CONSISTENT S p M /\
+                 MEM (Not p) M /\
+                 (!q. MEM q M ==> q SUBSENTENCE p)`
+
+
+g `!S W R p. ~ [S . {} |~ p] /\
+             (W,R) IN GEN_STANDARD_FRAME S p
+             ==>
+             ~holds_in (W,R) p`;;
+e (INTRO_TAC "!S W R p; p_not_theor in_standard_frame");;
+e (REWRITE_TAC[holds_in; NOT_FORALL_THM; NOT_IMP; IN_ELIM_THM]);;
+e (EXISTS_TAC `\a M. Atom a SUBFORMULA p /\ MEM (Atom a) M`);;
+e (DESTRUCT_TAC "@M. max mem subf" (MATCH_MP NONEMPTY_MAXIMAL_CONSISTENT (ASSUME `~ [S . {} |~ p]`)));;
+e (EXISTS_TAC `M:form list` THEN ASM_REWRITE_TAC[]);;
+e (SUBGOAL_THEN `GEN_STANDARD_MODEL S p (W,R) (\a M. Atom a SUBFORMULA p /\ MEM (Atom a) M) ` MP_TAC);;
+e (ASM_MESON_TAC[GEN_STANDARD_MODEL_DEF]);;
+e (INTRO_TAC "standard_model");;
+e CONJ_TAC;;
+e (HYP_TAC "in_standard_frame" (REWRITE_RULE[IN_GEN_STANDARD_FRAME]));;
+e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
+e (MP_TAC (ISPECL
+     [`S: form ->bool`;
+      `W: (form)list->bool`;
+      `R: (form)list-> (form)list ->bool`;
+      `p:form`;
+      `(\a M. Atom a SUBFORMULA p /\ MEM (Atom a) M):((char)list->(form)list->bool)`;
+      `p:form`] GEN_TRUTH_LEMMA));;
+e (ANTS_TAC );;
+e (ASM_REWRITE_TAC[SUBFORMULA_REFL]);;
+e (DISCH_THEN (MP_TAC o SPEC `M:form list`));;
+e ANTS_TAC;;
+e (HYP_TAC "standard_model" (REWRITE_RULE[GEN_STANDARD_MODEL_DEF; IN_GEN_STANDARD_FRAME]));;
+e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
+e (DISCH_THEN (SUBST1_TAC o GSYM));;
+e (ASM_MESON_TAC[MAXIMAL_CONSISTENT; CONSISTENT_NC]);;
+let GEN_COUNTERMODEL_ALT = top_thm();;
+```
+
+Given the fully parametrised `GEN_COUNTERMODEL_ALT` and `SF_IN_STANDARD_S_FRAME`, the completeness theorems for every $S$ follow and their proofs are so brief that we can present them here.
+
+#### Completeness of K in `k_completeness.ml`.
+```
+g `!p. FINITE_FRAME:(form list->bool)#(form list->form list->bool)->bool |= p
+       ==> [{} . {} |~ p]`;;
+e (GEN_TAC THEN GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] );;
+e (INTRO_TAC "p_not_theor");;
+e (REWRITE_TAC[valid; NOT_FORALL_THM]);;
+e (EXISTS_TAC `({M | MAXIMAL_CONSISTENT {} p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+                K_STANDARD_REL p)`);;
+e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC );;
+e (MATCH_MP_TAC K_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT {} p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+                  K_STANDARD_REL p) IN GEN_STANDARD_FRAME {} p`
+                 MP_TAC);;
+e (ASM_MESON_TAC[KF_IN_STANDARD_K_FRAME; K_STANDARD_FRAME_DEF]);;
+e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);;
+let K_COMPLETENESS_THM = top_thm ();;
+```
+
+#### Completeness of T in `t_completeness.ml`
+```
+g `!p. RF:(form list->bool)#(form list->form list->bool)->bool |= p
+       ==> [T_AX . {} |~ p]`;;
+e (GEN_TAC THEN GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] );;
+e (INTRO_TAC "p_not_theor");;
+e (REWRITE_TAC[valid; NOT_FORALL_THM]);;
+e (EXISTS_TAC `({M | MAXIMAL_CONSISTENT T_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+                T_STANDARD_REL p)`);;
+e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC );;
+e (MATCH_MP_TAC RF_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT T_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+                  T_STANDARD_REL p) IN GEN_STANDARD_FRAME T_AX p`
+                 MP_TAC);;
+e (ASM_MESON_TAC[RF_IN_T_STANDARD_FRAME; T_STANDARD_FRAME_DEF]);;
+e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);;
+let T_COMPLETENESS_THM = top_thm ();;
+```
+
+#### Completeness of K4 in `k4_completeness.ml`
+```
+g `!p. TF:(form list->bool)#(form list->form list->bool)->bool |= p
+       ==> [K4_AX . {} |~ p]`;;
+e (GEN_TAC THEN GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] );;
+e (INTRO_TAC "p_not_theor");;
+e (REWRITE_TAC[valid; NOT_FORALL_THM]);;
+e (EXISTS_TAC `({M | MAXIMAL_CONSISTENT K4_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+                K4_STANDARD_REL p)`);;
+e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC );;
+e (MATCH_MP_TAC TF_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT K4_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+                  K4_STANDARD_REL p) IN GEN_STANDARD_FRAME K4_AX p`
+                 MP_TAC);;
+e (ASM_MESON_TAC[K4F_IN_K4_STANDARD_FRAME; K4_STANDARD_FRAME_DEF]);;
+e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);;
+let K4_COMPLETENESS_THM = top_thm ();;
+```
+
+#### Completeness of GL in `gl_completeness.ml`
+
+```
+ g `!p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p
+        ==> [GL_AX . {} |~ p]`;;
+e (GEN_TAC THEN GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] );;
+e (INTRO_TAC "p_not_theor");;
+e (REWRITE_TAC[valid; NOT_FORALL_THM]);;
+e (EXISTS_TAC `({M | MAXIMAL_CONSISTENT GL_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+               GL_STANDARD_REL p)`);;
+e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC );;
+e (MATCH_MP_TAC ITF_MAXIMAL_CONSISTENT);;
+e (ASM_REWRITE_TAC[]);;
+e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT GL_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
+                   GL_STANDARD_REL p) IN GEN_STANDARD_FRAME GL_AX p`
+                  MP_TAC);;
+e (ASM_MESON_TAC[GLF_IN_GL_STANDARD_FRAME; GL_STANDARD_FRAME_DEF]);;
+e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);;
+let GL_COMPLETENESS_THM = top_thm ();;
 ```
 
-Completeness of GL in `gl_completness.ml`
-This proof uses the `GL_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completness theorem for GL is completely parametrized.
+###  Modal completeness for models on a generic (infinite) domain.
+Observe that our proof of completeness has an issue: it requires that `CORR S` is not just a set of correspondent frames but a set of correspondent frames with has a **finite** domain that is **a set formulas' lists**. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we can quickly generalise each completeness theorem for models with infinite worlds. 
+
+
+In `gen_completeness`.
 ```
-GL_COMPLETENESS_THM
-|- !p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p
-       ==> [GL_AX . {} |~ p]
+GEN_LEMMA_FOR_GEN_COMPLETENESS
+|- `!S. INFINITE (:A)
+       ==> !p. CORR S:(A->bool)#(A->A->bool)->bool |= p
+            ==> CORR S:(form list->bool)#(form list->form list->bool)->bool |= p`;;
 ```
-
-###  Modal completeness for models on a generic (infinite) domain.
-These theorems generalize the previous ones for models with infinite worlds.
+As corollaries of `GEN_LEMMA_FOR_GEN_COMPLETENESS`, in the specific files.
 ```
 K_COMPLETENESS_THM_GEN
-|- !p. INFINITE (:A) /\ K_FRAME:(A->bool)#(A->A->bool)->bool |= p
-       ==> [{} . {} |~ p]
+|- `!p. INFINITE (:A) /\ FINITE_FRAME:(A->bool)#(A->A->bool)->bool |= p
+       ==> [{} . {} |~ p]`
+
+T_COMPLETENESS_THM_GEN
+|- `!p. INFINITE (:A) /\ RF:(A->bool)#(A->A->bool)->bool |= p
+       ==> [T_AX . {} |~ p]`
+
+K4_COMPLETENESS_THM_GEN
+|- `!p. INFINITE (:A) /\ TF:(A->bool)#(A->A->bool)->bool |= p
+       ==> [K4_AX . {} |~ p]`
 
 GL_COMPLETENESS_THM_GEN
 |- !p. INFINITE (:A) /\ ITF:(A->bool)#(A->A->bool)->bool |= p
@@ -361,6 +843,46 @@ k_COUNTERMODEL_FINITE_SETS
 |- !p. ~[{} . {} |~ p] ==> ~holds_in (K_STDWORLDS p, K_STDREL p) p
 ```
 
+### In T
+Construction of the countermodels.
+```
+let T_STDWORLDS_RULES,T_STDWORLDS_INDUCT,T_STDWORLDS_CASES =
+  new_inductive_set
+  `!M. MAXIMAL_CONSISTENT T_AX p M /\
+       (!q. MEM q M ==> q SUBSENTENCE p)
+       ==> set_of_list M IN T_STDWORLDS p`;;
+
+let T_STDREL_RULES,T_STDREL_INDUCT,T_STDREL_CASES = new_inductive_definition
+  `!w1 w2. T_STANDARD_REL p w1 w2
+           ==> T_STDREL p (set_of_list w1) (set_of_list w2)`;;
+```
+
+Theorem of existence of the finite countermodel.
+```
+T_COUNTERMODEL_FINITE_SETS
+|- `!p. ~ [T_AX . {} |~ p] ==> ~holds_in (T_STDWORLDS p, T_STDREL p) p`
+```
+
+### In K4
+Construction of the countermodels.
+```
+let K4_STDWORLDS_RULES,K4_STDWORLDS_INDUCT,K4_STDWORLDS_CASES =
+  new_inductive_set
+  `!M. MAXIMAL_CONSISTENT K4_AX p M /\
+       (!q. MEM q M ==> q SUBSENTENCE p)
+       ==> set_of_list M IN K4_STDWORLDS p`;;
+
+let K4_STDREL_RULES,K4_STDREL_INDUCT,K4_STDREL_CASES = new_inductive_definition
+  `!w1 w2. K4_STANDARD_REL p w1 w2
+           ==> K4_STDREL p (set_of_list w1) (set_of_list w2)`;;
+```
+
+Theorem of existence of the finite countermodel.
+```
+K4_COUNTERMODEL_FINITE_SETS
+|- `!p. ~ [K4_AX . {} |~ p] ==> ~holds_in (K4_STDWORLDS p, K4_STDREL p) p`
+```
+
 ### In GL
 Construction of the countermodels.
 ```
@@ -394,6 +916,17 @@ K_RULE `!a b. [{} . {} |~ Box (a && b) <-> Box a && Box b]`;;
 K_RULE `!a b. [{} . {} |~ Box a || Box b --> Box (a || b)]`;;
 ```
 
+
+### In T
+
+Our tactic `T_TAC` and its associated rule `T_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrates that in future works we will be able to automatically prove theorems in the modal logic T.
+
+
+### In K4
+
+Our tactic `K4_TAC` and its associated rule `K4_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrates that in future works we will be able to  automatically prove theorems in the modal logic K4.
+
+
 ### In GL
 
 Our tactic `GL_TAC` and its associated rule `GL_RULE` can automatically prove theorems in the modal logic GL.
@@ -454,4 +987,4 @@ For any arithmetical sentences p q, p is equivalent to unprovability of q --> p
 let GL_arithmetical_fixpoint = time GL_RULE
   `!p q. [GL_AX . {} |~ Dotbox (p <-> Not (Box (q --> p))) <->
                         Dotbox (p <-> Diam q)]`;;
-```
\ No newline at end of file
+```