Duzy commit ze smieciami

28 files changed, 0 insertions, 782 deletions

diff --git a/Semestr 3/pf/lista5/proof/Makefile b/Semestr 3/pf/lista5/proof/Makefile
deleted file mode 100644
index 0f64038..0000000
--- a/Semestr 3/pf/lista5/proof/Makefile
+++ /dev/null
@@ -1,22 +0,0 @@
-SOURCES = logic.ml logic.mli proof.mli proof.ml logic.mllib
-CMFILES = logic.cma logic.cmi proof.cmi
-.PHONY: all clean build
-
-all: logic.cma logic.cmi proof.cmi
-
-build: $(SOURCES)
-	rm -f $(CMFILES)
-	ocamlbuild logic.cma
-
-logic.cma: build
-	cp _build/$@ $@
-
-logic.cmi: build
-	cp _build/$@ $@
-
-proof.cmi: build
-	cp _build/$@ $@
-
-clean:
-	rm -f $(CMFILES)
-	ocamlbuild -clean
diff --git a/Semestr 3/pf/lista5/proof/README b/Semestr 3/pf/lista5/proof/README
deleted file mode 100644
index 5fda955..0000000
--- a/Semestr 3/pf/lista5/proof/README
+++ /dev/null
@@ -1,30 +0,0 @@
-Szablon do listy 5 z Programowania funkcyjnego w grupach mabi, mbu, ppo i efes.
-
-Zarówno plik README, jak i źródła wykorzystują kodowanie znaków UTF-8.
-Jeśli nie wyświetlają się one dobrze na Twoim komputerze, zadbaj o to,
-by Twój edytor używał kodowania znaków UTF-8. Jeśli Twój edytor tego
-nie potrafi, zmień edytor.
-
-Pliki logic.mli, logic.ml, proof.mli, proof.ml definiują bibliotekę,
-którą łatwo skompilować poleceniem
-
-$ make
-
-Pliki logic.mli i logic.ml to szablon listy 4, więc należy je zastąpić
-rozwiązaniami tej listy.
-
-Żeby moduły definiowane przez tą bibliotekę były widoczne w interpreterze,
-należy przekazać plik logic.cma jako parametr do interpretera:
-
-$ utop logic.cma
-
-Jeśli masz problemy ze skompilowaniem biblioteki, możesz zawsze skompilować ją
-ręcznie, choć nie jest to najwygodniejsza metoda:
-
-$ ocamlc -c logic.mli
-$ ocamlc -c logic.ml
-$ ocamlc -c proof.mli
-$ ocamlc -c proof.ml
-$ ocamlc -a -o logic.cma logic.cmo proof.cmo
-
-Pamiętaj, że po każdej zmianie należy przekompilować bibliotekę.
diff --git a/Semestr 3/pf/lista5/proof/_build/_digests b/Semestr 3/pf/lista5/proof/_build/_digests
deleted file mode 100644
index ccd3d21..0000000
--- a/Semestr 3/pf/lista5/proof/_build/_digests
+++ /dev/null
@@ -1,14 +0,0 @@
-"Rule: ocaml: mllib & cmo* -> cma (%=logic )": "\140\207$\221\162s\006\158\014\193x\211\213\214?\207"
-"Rule: ocaml dependencies mli (%=proof )": "[]+Z#ML\231B<\205\129iN)F"
-"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/logic.ml": "\150B>+\t\250\189\162{\249\180\159\247\254\227|"
-"Rule: ocaml dependencies ml (%=logic )": "\189H\162<i\136\029\211n.\248\139\156L\019\131"
-"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/logic.mli": "\144T\172\t\250\250\t\020qGU\157\247\251M\b"
-"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/proof.ml": "w\002pJ9\208\200;\2479Mu\163u\t\227"
-"Rule: ocaml: ml & cmi -> cmo (%=logic )": " L\147\\Y\152\139<e\236\027\014pm\030\017"
-"Rule: ocaml: mli -> cmi (%=proof )": "\223\208\252\178\001\197b\158\237w\007\216\152\174\015\172"
-"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/proof.mli": ";\002\022\169V-\145\129\138\nkd\248\164\253\188"
-"Rule: ocaml: ml & cmi -> cmo (%=proof )": "\159\157\219\164\172\158\006.\150\138\167;/\182\b\163"
-"Rule: ocaml: mli -> cmi (%=logic )": "\170\192\216\b\023\138!\200EW\017\002\179\007fC"
-"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/logic.mllib": ",2\194\127\202\253h\245\152ps`\018\195l\230"
-"Rule: ocaml dependencies mli (%=logic )": "|\128\193\029\172\176V6EV\145\157\148J\007\232"
-"Rule: ocaml dependencies ml (%=proof )": "\151?\155\014\169[\138~\179\016\005\026v\021O\""
diff --git a/Semestr 3/pf/lista5/proof/_build/_log b/Semestr 3/pf/lista5/proof/_build/_log
deleted file mode 100644
index 283f2b6..0000000
--- a/Semestr 3/pf/lista5/proof/_build/_log
+++ /dev/null
@@ -1,20 +0,0 @@
-### Starting build.
-# Target: logic.mli.depends, tags: { extension:mli, file:logic.mli, ocaml, ocamldep, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules logic.mli > logic.mli.depends # cached
-# Target: logic.cmi, tags: { byte, compile, extension:mli, file:logic.mli, interf, ocaml, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o logic.cmi logic.mli # cached
-# Target: logic.ml.depends, tags: { extension:ml, file:logic.ml, ocaml, ocamldep, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules logic.ml > logic.ml.depends
-# Target: proof.mli.depends, tags: { extension:mli, file:proof.mli, ocaml, ocamldep, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules proof.mli > proof.mli.depends # cached
-# Target: proof.cmi, tags: { byte, compile, extension:mli, file:proof.mli, interf, ocaml, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o proof.cmi proof.mli # cached
-# Target: proof.ml.depends, tags: { extension:ml, file:proof.ml, ocaml, ocamldep, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules proof.ml > proof.ml.depends # cached
-# Target: proof.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:proof.cmo, file:proof.ml, implem, ocaml, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o proof.cmo proof.ml # cached
-# Target: logic.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:logic.cmo, file:logic.ml, implem, ocaml, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o logic.cmo logic.ml
-# Target: logic.cma, tags: { byte, extension:cma, file:logic.cma, library, link, ocaml, quiet, traverse }
-/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -a logic.cmo proof.cmo -o logic.cma
-# Compilation successful.
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cma b/Semestr 3/pf/lista5/proof/_build/logic.cma
deleted file mode 100644
index 2040e52..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.cma
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cmi b/Semestr 3/pf/lista5/proof/_build/logic.cmi
deleted file mode 100644
index d9d951f..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.cmi
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cmo b/Semestr 3/pf/lista5/proof/_build/logic.cmo
deleted file mode 100644
index 7fcc4f9..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.cmo
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.ml b/Semestr 3/pf/lista5/proof/_build/logic.ml
deleted file mode 100644
index 27140d5..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-type formula = False | Var of string | Imp of formula * formula
-
-let rec string_of_formula f =
-  match f with
-    False -> "⊥"
-  | Var str -> str
-  | Imp (f1, f2) -> let str1 = string_of_formula f1 in
-    (match f1 with
-       Imp (_, _) -> "(" ^ str1 ^ ")"
-     | _ -> str1) ^ " ⇒ " ^ string_of_formula f2
-;;
-(* match (f1, f2) with
-   | (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *)
-
-let pp_print_formula fmtr f =
-  Format.pp_print_string fmtr (string_of_formula f)
-
-type theorem = { assump : formula list; concl : formula }
-
-let assumptions thm = thm.assump
-let consequence thm = thm.concl
-
-let pp_print_theorem fmtr thm =
-  let open Format in
-  pp_open_hvbox fmtr 2;
-  begin match assumptions thm with
-    | [] -> ()
-    | f :: fs ->
-      pp_print_formula fmtr f;
-      fs |> List.iter (fun f ->
-          pp_print_string fmtr ",";
-          pp_print_space fmtr ();
-          pp_print_formula fmtr f);
-      pp_print_space fmtr ()
-  end;
-  pp_open_hbox fmtr ();
-  pp_print_string fmtr "⊢";
-  pp_print_space fmtr ();
-  pp_print_formula fmtr (consequence thm);
-  pp_close_box fmtr ();
-  pp_close_box fmtr ()
-
-let by_assumption f =
-  { assump=[f]; concl=f }
-
-let imp_i f thm =
-  { assump=(List.filter ((<>) f) thm.assump); concl=(Imp (f, thm.concl)) }
-
-let imp_e th1 th2 =
-  match th1.concl with
-  | False | Var _ -> failwith "th1 conclusion is not implication"
-  | Imp (phi, psi) -> if phi <> th2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else  
-      { assump = th1.assump @ th2.assump; concl = psi}
-
-let bot_e f thm =
-  match thm with
-  | {assump=ass; concl=False} -> {assump=ass; concl=f}
-  | _ -> failwith "thm conclusion is not False"
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.ml.depends b/Semestr 3/pf/lista5/proof/_build/logic.ml.depends
deleted file mode 100644
index 5169b43..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.ml.depends
+++ /dev/null
@@ -1 +0,0 @@
-logic.ml: Format List
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mli b/Semestr 3/pf/lista5/proof/_build/logic.mli
deleted file mode 100644
index afbdc7d..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(** reprezentacja formuł *)
-type formula = False | Var of string | Imp of formula * formula
-
-val pp_print_formula : Format.formatter -> formula -> unit
-
-(** reprezentacja twierdzeń *)
-type theorem
-
-(** założenia twierdzenia *)
-val assumptions : theorem -> formula list
-(** teza twierdzeni *)
-val consequence : theorem -> formula
-
-val pp_print_theorem : Format.formatter -> theorem -> unit
-
-(** by_assumption f konstuuje następujący dowód
-
-    -------(Ax)
-    {f} ⊢ f  *)
-val by_assumption : formula -> theorem
-
-(** imp_i f thm konstuuje następujący dowód
-
-       thm
-      Γ ⊢ φ
-    ---------------(→I)
-    Γ \ {f} ⊢ f → φ *)
-val imp_i : formula -> theorem -> theorem
-
-(** imp_e thm1 thm2 konstuuje następujący dowód
-
-    thm1      thm2
-    Γ ⊢ φ → ψ    Δ ⊢ φ 
-    ------------------(→E)
-    Γ ∪ Δ ⊢ ψ *)
-val imp_e : theorem -> theorem -> theorem
-
-(** bot_e f thm konstruuje następujący dowód
-
-    thm
-    Γ ⊢ ⊥
-    -----(⊥E)
-    Γ ⊢ f *)
-val bot_e : formula -> theorem -> theorem
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mli.depends b/Semestr 3/pf/lista5/proof/_build/logic.mli.depends
deleted file mode 100644
index 3c54482..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.mli.depends
+++ /dev/null
@@ -1 +0,0 @@
-logic.mli: Format
diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mllib b/Semestr 3/pf/lista5/proof/_build/logic.mllib
deleted file mode 100644
index 00433f8..0000000
--- a/Semestr 3/pf/lista5/proof/_build/logic.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Logic
-Proof
diff --git a/Semestr 3/pf/lista5/proof/_build/ocamlc.where b/Semestr 3/pf/lista5/proof/_build/ocamlc.where
deleted file mode 100644
index 49511f0..0000000
--- a/Semestr 3/pf/lista5/proof/_build/ocamlc.where
+++ /dev/null
@@ -1 +0,0 @@
-/home/fmalinka/.opam/4.11.1/lib/ocaml
diff --git a/Semestr 3/pf/lista5/proof/_build/proof.cmi b/Semestr 3/pf/lista5/proof/_build/proof.cmi
deleted file mode 100644
index 47417e3..0000000
--- a/Semestr 3/pf/lista5/proof/_build/proof.cmi
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/_build/proof.cmo b/Semestr 3/pf/lista5/proof/_build/proof.cmo
deleted file mode 100644
index 674156d..0000000
--- a/Semestr 3/pf/lista5/proof/_build/proof.cmo
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/_build/proof.ml b/Semestr 3/pf/lista5/proof/_build/proof.ml
deleted file mode 100644
index 83ee71a..0000000
--- a/Semestr 3/pf/lista5/proof/_build/proof.ml
+++ /dev/null
@@ -1,109 +0,0 @@
-open Logic
-
-type context = (string * formula) list
-type goalDesc = context * formula
-
-type proof = 
-  | Assumption of theorem
-  | ImpInsert of theorem * proof
-  | ImpErase of theorem * proof * proof
-  | Contradiction of theorem * proof
-  | Whole of goalDesc
-
-type goal (* = TODO: tu wpisz swoją definicję *)
-
-let qed pf =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let numGoals pf =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let goals pf =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let proof g f =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let goal pf =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let focus n pf =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let unfocus gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let next gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let prev gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let intro name gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let apply f gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let apply_thm thm gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let apply_assm name gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let pp_print_proof fmtr pf =
-  let ngoals = numGoals pf
-  and goals = goals pf
-  in if ngoals = 0
-  then Format.pp_print_string fmtr "No more subgoals"
-  else begin
-    Format.pp_open_vbox fmtr (-100);
-    Format.pp_open_hbox fmtr ();
-    Format.pp_print_string fmtr "There are";
-    Format.pp_print_space fmtr ();
-    Format.pp_print_int fmtr ngoals;
-    Format.pp_print_space fmtr ();
-    Format.pp_print_string fmtr "subgoals:";
-    Format.pp_close_box fmtr ();
-    Format.pp_print_cut fmtr ();
-    goals |> List.iteri (fun n (_, f) ->
-        Format.pp_print_cut fmtr ();
-        Format.pp_open_hbox fmtr ();
-        Format.pp_print_int fmtr (n + 1);
-        Format.pp_print_string fmtr ":";
-        Format.pp_print_space fmtr ();
-        pp_print_formula fmtr f;
-        Format.pp_close_box fmtr ());
-    Format.pp_close_box fmtr ()
-  end
-
-let pp_print_goal fmtr gl =
-  let (g, f) = goal gl
-  in
-  Format.pp_open_vbox fmtr (-100);
-  g |> List.iter (fun (name, f) ->
-      Format.pp_print_cut fmtr ();
-      Format.pp_open_hbox fmtr ();
-      Format.pp_print_string fmtr name;
-      Format.pp_print_string fmtr ":";
-      Format.pp_print_space fmtr ();
-      pp_print_formula fmtr f;
-      Format.pp_close_box fmtr ());
-  Format.pp_print_cut fmtr ();
-  Format.pp_print_string fmtr (String.make 40 '=');
-  Format.pp_print_cut fmtr ();
-  pp_print_formula fmtr f;
-  Format.pp_close_box fmtr ()
diff --git a/Semestr 3/pf/lista5/proof/_build/proof.ml.depends b/Semestr 3/pf/lista5/proof/_build/proof.ml.depends
deleted file mode 100644
index 85d6816..0000000
--- a/Semestr 3/pf/lista5/proof/_build/proof.ml.depends
+++ /dev/null
@@ -1 +0,0 @@
-proof.ml: Format List Logic String
diff --git a/Semestr 3/pf/lista5/proof/_build/proof.mli b/Semestr 3/pf/lista5/proof/_build/proof.mli
deleted file mode 100644
index ad16a08..0000000
--- a/Semestr 3/pf/lista5/proof/_build/proof.mli
+++ /dev/null
@@ -1,86 +0,0 @@
-open Logic
-
-type context = (string * formula) list
-type goalDesc = context * formula
-
-type proof
-type goal
-
-(** Zamienia ukończony dowód na twierdzenie *)
-val qed : proof -> theorem
-
-(** Zwraca liczbę pozostałych w dowodze celów (0 <-> dowód jest gotowy i można go zakończyć) *)
-val numGoals : proof -> int
-
-(** Zwraca listę celów w danym dowodzie *)
-val goals : proof -> goalDesc list
-
-
-(** Tworzy pusty dowód podanego twierdzenia *)
-val proof : context -> formula -> proof
-
-(** Zwraca (assm, phi), gdzie assm oraz phi to odpowiednio dostępne
-    założenia oraz formuła do udowodnienia w aktywnym podcelu *)
-val goal : goal -> goalDesc
-
-(** Ustawia aktywny cel w danym dowodzie *)
-val focus : int -> proof -> goal
-
-(** Zapomina informację o celu *)
-val unfocus : goal -> proof
-
-(** Zmienia (cyklicznie) aktywny cel na następny/poprzedni *)
-val next : goal -> goal
-val prev : goal -> goal
-
-(** Wywołanie intro name pf odpowiada regule wprowadzania implikacji.
-    To znaczy aktywna dziura wypełniana jest regułą:
-
-    (nowy aktywny cel)
-    (name,ψ) :: Γ ⊢ φ
-    -----------------(→I)
-       Γ ⊢ ψ → φ
-
-    Jeśli aktywny cel nie jest implikacją, wywołanie kończy się błędem *)
-val intro : string -> goal -> goal
-
-(** Wywołanie apply ψ₀ pf odpowiada jednocześnie eliminacji implikacji
-    i eliminacji fałszu. Tzn. jeśli do udowodnienia jest φ, a ψ₀ jest
-    postaci ψ₁ → ... → ψn → φ to aktywna dziura wypełniana jest regułami
-
-    (nowy aktywny cel) (nowy cel)
-        Γ ⊢ ψ₀          Γ ⊢ ψ₁
-        ----------------------(→E)  (nowy cel)
-                ...                   Γ ⊢ ψn
-                ----------------------------(→E)
-                            Γ ⊢ φ
-
-    Natomiast jeśli ψ₀ jest postaci ψ₁ → ... → ψn → ⊥ to aktywna dziura
-    wypełniana jest regułami
-
-    (nowy aktywny cel) (nowy cel)
-        Γ ⊢ ψ₀          Γ ⊢ ψ₁
-        ----------------------(→E)  (nowy cel)
-                ...                   Γ ⊢ ψn
-                ----------------------------(→E)
-                            Γ ⊢ ⊥
-                            -----(⊥E)
-                            Γ ⊢ φ *)
-val apply : formula -> goal -> goal
-
-(** Wywołanie `apply_thm thm pf` działa podobnie do
-    `apply (Logic.consequence thm) pf`, tyle że aktywna dziura od razu
-    jest wypełniana dowodem thm, a otrzymane drzewo nie jest
-    sfokusowane na żadnym z celów.
-*)
-
-val apply_thm : theorem -> goal -> proof
-
-(** Wywołanie `apply_assm name pf` działa tak jak
-    `apply (Logic.by_assumption f) pf`, gdzie f jest założeniem o
-    nazwie name
-*)
-val apply_assm : string -> goal -> proof
-
-val pp_print_proof : Format.formatter -> proof -> unit
-val pp_print_goal  : Format.formatter -> goal -> unit
diff --git a/Semestr 3/pf/lista5/proof/_build/proof.mli.depends b/Semestr 3/pf/lista5/proof/_build/proof.mli.depends
deleted file mode 100644
index e405b4e..0000000
--- a/Semestr 3/pf/lista5/proof/_build/proof.mli.depends
+++ /dev/null
@@ -1 +0,0 @@
-proof.mli: Format Logic
diff --git a/Semestr 3/pf/lista5/proof/_tags b/Semestr 3/pf/lista5/proof/_tags
deleted file mode 100644
index e69de29..0000000
--- a/Semestr 3/pf/lista5/proof/_tags
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/logic.cma b/Semestr 3/pf/lista5/proof/logic.cma
deleted file mode 100644
index 2040e52..0000000
--- a/Semestr 3/pf/lista5/proof/logic.cma
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/logic.cmi b/Semestr 3/pf/lista5/proof/logic.cmi
deleted file mode 100644
index d9d951f..0000000
--- a/Semestr 3/pf/lista5/proof/logic.cmi
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/logic.ml b/Semestr 3/pf/lista5/proof/logic.ml
deleted file mode 100644
index 234123e..0000000
--- a/Semestr 3/pf/lista5/proof/logic.ml
+++ /dev/null
@@ -1,142 +0,0 @@
-(* type formula = False | Var of string | Imp of formula * formula
-
-   let rec string_of_formula = function
-   | False -> "F"
-   | Var s -> s
-   | Imp (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")"
-   (* match (f1, f2) with
-   | (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *)
-
-   let pp_print_formula fmtr f =
-   Format.pp_print_string fmtr (string_of_formula f)
-
-   type verdict = { assump : formula list; concl : formula }
-
-   type theorem = 
-   | Assumption of verdict
-   | ImpInsert of verdict * theorem
-   | ImpErase of verdict * theorem * theorem
-   | Contradiction of verdict * theorem
-
-   let get_verdict thm = match thm with
-   | Assumption f -> f
-   | ImpInsert (v, _) | ImpErase (v, _, _) | Contradiction (v, _) -> v
-
-   let assumptions thm = (get_verdict thm).assump
-   let consequence thm = (get_verdict thm).concl
-
-   let pp_print_theorem fmtr thm =
-   let open Format in
-   pp_open_hvbox fmtr 2;
-   begin match assumptions thm with
-    | [] -> ()
-    | f :: fs ->
-      pp_print_formula fmtr f;
-      fs |> List.iter (fun f ->
-          pp_print_string fmtr ",";
-          pp_print_space fmtr ();
-          pp_print_formula fmtr f);
-      pp_print_space fmtr ()
-   end;
-   pp_open_hbox fmtr ();
-   pp_print_string fmtr "⊢";
-   pp_print_space fmtr ();
-   pp_print_formula fmtr (consequence thm);
-   pp_close_box fmtr ();
-   pp_close_box fmtr ()
-
-   let by_assumption f =
-   Assumption { assump=[f]; concl=f }
-
-   let imp_i f thm =
-   let premise = get_verdict thm
-   in ImpInsert ({assump=(List.filter ((<>) f) premise.assump); concl=(Imp (f, premise.concl))}, thm)
-
-   let imp_e th1 th2 =
-   let premise1 = get_verdict th1 in 
-   let premise2 = get_verdict th2 in
-   match premise1.concl with
-   | False | Var _ -> failwith "th1 conclusion is not implication"
-   | Imp (phi, psi) -> if phi <> premise2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else  
-      ImpErase ({assump=(premise1.assump @ premise2.assump); concl=(psi)}, th1, th2)
-
-   let bot_e f thm =
-   match get_verdict thm with
-   | {assump=ass; concl=False}-> (Contradiction ({assump=ass; concl=f}, thm))
-   | _ -> failwith "thm conclusion is not False"
-
-
-   let taut = (imp_i (Var "p") (by_assumption (Var "p")))
-   let taut2 = (imp_i (Var "p") (imp_i (Var "q") (by_assumption (Var "p"))))
-
-   let imppqr = Imp (Var "p", Imp (Var "q", Var "r"))
-   let imppq = Imp (Var "p", Var "q")
-   let imppr = Imp (Var "p", Var "r")
-   let taut3 = (imp_i (imppqr) (imp_i imppq (by_assumption imppr)))   *)
-
-
-
-type formula = False | Var of string | Imp of formula * formula
-
-let rec string_of_formula f =
-  match f with
-    False -> "⊥"
-  | Var str -> str
-  | Imp (f1, f2) -> let str1 = string_of_formula f1 in
-    (match f1 with
-       Imp (_, _) -> "(" ^ str1 ^ ")"
-     | _ -> str1) ^ " ⇒ " ^ string_of_formula f2
-;;
-(* match (f1, f2) with
-   | (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
-   | (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *)
-
-let pp_print_formula fmtr f =
-  Format.pp_print_string fmtr (string_of_formula f)
-
-type theorem = { assump : formula list; concl : formula }
-
-let assumptions thm = thm.assump
-let consequence thm = thm.concl
-
-let pp_print_theorem fmtr thm =
-  let open Format in
-  pp_open_hvbox fmtr 2;
-  begin match assumptions thm with
-    | [] -> ()
-    | f :: fs ->
-      pp_print_formula fmtr f;
-      fs |> List.iter (fun f ->
-          pp_print_string fmtr ",";
-          pp_print_space fmtr ();
-          pp_print_formula fmtr f);
-      pp_print_space fmtr ()
-  end;
-  pp_open_hbox fmtr ();
-  pp_print_string fmtr "⊢";
-  pp_print_space fmtr ();
-  pp_print_formula fmtr (consequence thm);
-  pp_close_box fmtr ();
-  pp_close_box fmtr ()
-
-let by_assumption f =
-  { assump=[f]; concl=f }
-
-let imp_i f thm =
-  { assump=(List.filter ((<>) f) thm.assump); concl=(Imp (f, thm.concl)) }
-
-let imp_e th1 th2 =
-  match th1.concl with
-  | False | Var _ -> failwith "th1 conclusion is not implication"
-  | Imp (phi, psi) -> if phi <> th2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else  
-      { assump = th1.assump @ th2.assump; concl = psi}
-
-let bot_e f thm =
-  match thm with
-  | {assump=ass; concl=False} -> {assump=ass; concl=f}
-  | _ -> failwith "thm conclusion is not False"
diff --git a/Semestr 3/pf/lista5/proof/logic.mli b/Semestr 3/pf/lista5/proof/logic.mli
deleted file mode 100644
index afbdc7d..0000000
--- a/Semestr 3/pf/lista5/proof/logic.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(** reprezentacja formuł *)
-type formula = False | Var of string | Imp of formula * formula
-
-val pp_print_formula : Format.formatter -> formula -> unit
-
-(** reprezentacja twierdzeń *)
-type theorem
-
-(** założenia twierdzenia *)
-val assumptions : theorem -> formula list
-(** teza twierdzeni *)
-val consequence : theorem -> formula
-
-val pp_print_theorem : Format.formatter -> theorem -> unit
-
-(** by_assumption f konstuuje następujący dowód
-
-    -------(Ax)
-    {f} ⊢ f  *)
-val by_assumption : formula -> theorem
-
-(** imp_i f thm konstuuje następujący dowód
-
-       thm
-      Γ ⊢ φ
-    ---------------(→I)
-    Γ \ {f} ⊢ f → φ *)
-val imp_i : formula -> theorem -> theorem
-
-(** imp_e thm1 thm2 konstuuje następujący dowód
-
-    thm1      thm2
-    Γ ⊢ φ → ψ    Δ ⊢ φ 
-    ------------------(→E)
-    Γ ∪ Δ ⊢ ψ *)
-val imp_e : theorem -> theorem -> theorem
-
-(** bot_e f thm konstruuje następujący dowód
-
-    thm
-    Γ ⊢ ⊥
-    -----(⊥E)
-    Γ ⊢ f *)
-val bot_e : formula -> theorem -> theorem
diff --git a/Semestr 3/pf/lista5/proof/logic.mllib b/Semestr 3/pf/lista5/proof/logic.mllib
deleted file mode 100644
index 00433f8..0000000
--- a/Semestr 3/pf/lista5/proof/logic.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Logic
-Proof
diff --git a/Semestr 3/pf/lista5/proof/proof.cmi b/Semestr 3/pf/lista5/proof/proof.cmi
deleted file mode 100644
index 47417e3..0000000
--- a/Semestr 3/pf/lista5/proof/proof.cmi
+++ /dev/null
diff --git a/Semestr 3/pf/lista5/proof/proof.ml b/Semestr 3/pf/lista5/proof/proof.ml
deleted file mode 100644
index 3cde679..0000000
--- a/Semestr 3/pf/lista5/proof/proof.ml
+++ /dev/null
@@ -1,116 +0,0 @@
-open Logic
-
-type context = (string * formula) list
-type goalDesc = context * formula
-
-type proof = 
-  | Whole of goalDesc
-  | Leaf of theorem
-  | ImpInsert of theorem * proof
-  | ImpErase of theorem * proof * proof
-  | Contradiction of theorem * proof
-
-type goal = Goal of (goalDesc list) * (goalDesc list) * proof
-
-let rec numGoals pf =
-  match pf with
-  | Whole _ -> 1
-  | Leaf _ -> 0
-  | ImpInsert (_, pf) | Contradiction (_, pf) -> numGoals pf 
-  | ImpErase (_, pf1, pf2) -> (numGoals pf1) + (numGoals pf2)
-
-let qed pf =
-  if (numGoals pf) <> 0 then failwith "proof not finished" else
-    match pf with
-    | Whole _ -> failwith "proof not finished"
-    | Leaf thm | ImpInsert (thm, _) | ImpErase (thm, _, _) | Contradiction (thm, _) -> thm
-
-let rec goals pf =
-  match pf with
-  | Whole gd -> [gd]
-  | Leaf _ -> []
-  | ImpInsert (_, pf) | Contradiction (_, pf) -> goals pf
-  | ImpErase (_, pf1, pf2) -> (goals pf1) @ (goals pf2) 
-
-let proof g f =
-  Whole (g, f)
-
-let goal (Goal (bef, aft, pf)) = 
-  if aft == [] then failwith "Goal is empty" else (List.hd aft)  
-
-let focus n pf =
-  let add_goal (Goal (bef, aft, pf)) gl =
-    Goal (bef, gl::aft, pf)
-  in let goal = List.fold_left add_goal (Goal ([], [], pf)) (goals pf) in
-
-  let unfocus gl =
-    (* TODO: zaimplementuj *)
-    failwith "not implemented"
-
-let next gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let prev gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let intro name gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let apply f gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let apply_thm thm gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let apply_assm name gl =
-  (* TODO: zaimplementuj *)
-  failwith "not implemented"
-
-let pp_print_proof fmtr pf =
-  let ngoals = numGoals pf
-  and goals = goals pf
-  in if ngoals = 0
-  then Format.pp_print_string fmtr "No more subgoals"
-  else begin
-    Format.pp_open_vbox fmtr (-100);
-    Format.pp_open_hbox fmtr ();
-    Format.pp_print_string fmtr "There are";
-    Format.pp_print_space fmtr ();
-    Format.pp_print_int fmtr ngoals;
-    Format.pp_print_space fmtr ();
-    Format.pp_print_string fmtr "subgoals:";
-    Format.pp_close_box fmtr ();
-    Format.pp_print_cut fmtr ();
-    goals |> List.iteri (fun n (_, f) ->
-        Format.pp_print_cut fmtr ();
-        Format.pp_open_hbox fmtr ();
-        Format.pp_print_int fmtr (n + 1);
-        Format.pp_print_string fmtr ":";
-        Format.pp_print_space fmtr ();
-        pp_print_formula fmtr f;
-        Format.pp_close_box fmtr ());
-    Format.pp_close_box fmtr ()
-  end
-
-let pp_print_goal fmtr gl =
-  let (g, f) = goal gl
-  in
-  Format.pp_open_vbox fmtr (-100);
-  g |> List.iter (fun (name, f) ->
-      Format.pp_print_cut fmtr ();
-      Format.pp_open_hbox fmtr ();
-      Format.pp_print_string fmtr name;
-      Format.pp_print_string fmtr ":";
-      Format.pp_print_space fmtr ();
-      pp_print_formula fmtr f;
-      Format.pp_close_box fmtr ());
-  Format.pp_print_cut fmtr ();
-  Format.pp_print_string fmtr (String.make 40 '=');
-  Format.pp_print_cut fmtr ();
-  pp_print_formula fmtr f;
-  Format.pp_close_box fmtr ()
diff --git a/Semestr 3/pf/lista5/proof/proof.mli b/Semestr 3/pf/lista5/proof/proof.mli
deleted file mode 100644
index 2c939fd..0000000
--- a/Semestr 3/pf/lista5/proof/proof.mli
+++ /dev/null
@@ -1,85 +0,0 @@
-open Logic
-
-type context = (string * formula) list
-type goalDesc = context * formula
-
-type proof
-type goal
-
-(** Zamienia ukończony dowód na twierdzenie *)
-val qed : proof -> theorem
-
-(** Zwraca liczbę pozostałych w dowodze celów (0 <-> dowód jest gotowy i można go zakończyć) *)
-val numGoals : proof -> int
-
-(** Zwraca listę celów w danym dowodzie *)
-val goals : proof -> goalDesc list
-
-(** Tworzy pusty dowód podanego twierdzenia *)
-val proof : context -> formula -> proof
-
-(** Zwraca (assm, phi), gdzie assm oraz phi to odpowiednio dostępne
-    założenia oraz formuła do udowodnienia w aktywnym podcelu *)
-val goal : goal -> goalDesc
-
-(** Ustawia aktywny cel w danym dowodzie *)
-val focus : int -> proof -> goal
-
-(** Zapomina informację o celu *)
-val unfocus : goal -> proof
-
-(** Zmienia (cyklicznie) aktywny cel na następny/poprzedni *)
-val next : goal -> goal
-val prev : goal -> goal
-
-(** Wywołanie intro name pf odpowiada regule wprowadzania implikacji.
-    To znaczy aktywna dziura wypełniana jest regułą:
-
-    (nowy aktywny cel)
-    (name,ψ) :: Γ ⊢ φ
-    -----------------(→I)
-       Γ ⊢ ψ → φ
-
-    Jeśli aktywny cel nie jest implikacją, wywołanie kończy się błędem *)
-val intro : string -> goal -> goal
-
-(** Wywołanie apply ψ₀ pf odpowiada jednocześnie eliminacji implikacji
-    i eliminacji fałszu. Tzn. jeśli do udowodnienia jest φ, a ψ₀ jest
-    postaci ψ₁ → ... → ψn → φ to aktywna dziura wypełniana jest regułami
-
-    (nowy aktywny cel) (nowy cel)
-        Γ ⊢ ψ₀          Γ ⊢ ψ₁
-        ----------------------(→E)  (nowy cel)
-                ...                   Γ ⊢ ψn
-                ----------------------------(→E)
-                            Γ ⊢ φ
-
-    Natomiast jeśli ψ₀ jest postaci ψ₁ → ... → ψn → ⊥ to aktywna dziura
-    wypełniana jest regułami
-
-    (nowy aktywny cel) (nowy cel)
-        Γ ⊢ ψ₀          Γ ⊢ ψ₁
-        ----------------------(→E)  (nowy cel)
-                ...                   Γ ⊢ ψn
-                ----------------------------(→E)
-                            Γ ⊢ ⊥
-                            -----(⊥E)
-                            Γ ⊢ φ *)
-val apply : formula -> goal -> goal
-
-(** Wywołanie `apply_thm thm pf` działa podobnie do
-    `apply (Logic.consequence thm) pf`, tyle że aktywna dziura od razu
-    jest wypełniana dowodem thm, a otrzymane drzewo nie jest
-    sfokusowane na żadnym z celów.
-*)
-
-val apply_thm : theorem -> goal -> proof
-
-(** Wywołanie `apply_assm name pf` działa tak jak
-    `apply (Logic.by_assumption f) pf`, gdzie f jest założeniem o
-    nazwie name
-*)
-val apply_assm : string -> goal -> proof
-
-val pp_print_proof : Format.formatter -> proof -> unit
-val pp_print_goal  : Format.formatter -> goal -> unit