fitch_first_order.v

(* generated by Ott 0.25 from: fitch_first_order.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Ott.ott_list_core.


Require Export dyadic_ordered.
Require Export FMapInterface.

Require Export String.
Require Import Ascii.
Hint Resolve ascii_dec : ott_coq_equality.

Module FitchFirstOrder
 (ST : SpecType) (SUOT : SpecUsualOrderedType ST)
 (DST : DyadicSpecType ST) (SUOTD : SpecUsualOrderedType DST)
 (Map : FMapInterface.S with Module E := SUOTD).

Definition x := string. (*r variable *)
Lemma eq_x: forall (x' y : x), {x' = y} + {x' <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_x : ott_coq_equality.
Definition f := string. (*r function name *)
Lemma eq_f: forall (x y : f), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_f : ott_coq_equality.
Definition c := string. (*r constant name *)
Lemma eq_c: forall (x y : c), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_c : ott_coq_equality.
Definition P := string. (*r predicate name *)
Lemma eq_P: forall (x y : P), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_P : ott_coq_equality.
Definition l := SUOT.t. (*r proof entry label *)
Definition n := nat. (*r index variable (subscript) *)
Lemma eq_n: forall (x y : n), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_n : ott_coq_equality.

Inductive t : Set :=  (*r term *)
 | t_var (x5:x)
 | t_const (c5:c)
 | t_func (f5:f) (_:list t).

Inductive justification : Type :=  (*r derivation justification *)
 | justification_premise : justification
 | justification_lem : justification
 | justification_copy (l5:l)
 | justification_andi (l5:l) (l':l)
 | justification_ande1 (l5:l)
 | justification_ande2 (l5:l)
 | justification_ori1 (l5:l)
 | justification_ori2 (l5:l)
 | justification_impe (l5:l) (l':l)
 | justification_nege (l5:l) (l':l)
 | justification_conte (l5:l)
 | justification_negnegi (l5:l)
 | justification_negnege (l5:l)
 | justification_mt (l5:l) (l':l)
 | justification_impi (l5:l) (l':l)
 | justification_negi (l5:l) (l':l)
 | justification_ore (l1:l) (l2:l) (l3:l) (l4:l) (l5:l)
 | justification_pbc (l5:l) (l':l)
 | justification_eqi : justification
 | justification_eqe (l5:l) (l':l)
 | justification_alli (l5:l) (l':l)
 | justification_alle (l5:l)
 | justification_exi (l5:l)
 | justification_exe (l1:l) (l2:l) (l3:l).

Inductive fm : Set :=  (*r first-order formula *)
 | fm_pred (P5:P) (_:list t)
 | fm_eq (t5:t) (t':t)
 | fm_neg (fm5:fm)
 | fm_and (fm5:fm) (fm':fm)
 | fm_or (fm5:fm) (fm':fm)
 | fm_imp (fm5:fm) (fm':fm)
 | fm_forall (x5:x) (fm5:fm)
 | fm_ex (x5:x) (fm5:fm)
 | fm_cont : fm.

Inductive reason : Type := 
 | reason_assumption : reason
 | reason_justification (justification5:justification).

Inductive fmlist : Set :=  (*r list of first-order formulas *)
 | fmlist_list (_:list fm).

Inductive derivation : Type :=  (*r derivation in proof *)
 | derivation_deriv (l5:l) (fm5:fm) (reason5:reason)
 | derivation_var (l5:l) (x5:x)
 | derivation_var_assumption (l5:l) (x5:x) (fm5:fm).

Inductive judgment : Set :=  (*r judgment *)
 | judgment_follows (fmlist5:fmlist) (fm5:fm).

Inductive proof : Type :=  (*r proof *)
 | proof_entries (_:list entry)
with entry : Type :=  (*r proof entry *)
 | entry_derivation (derivation5:derivation)
 | entry_box (proof5:proof)
 | entry_invalid : entry.

Inductive dyadicfm : Set := 
 | dyadicfm_fm (fm5:fm)
 | dyadicfm_fm_fm (fm5:fm) (fm':fm)
 | dyadicfm_var_fm (x5:x) (fm5:fm)
 | dyadicfm_var_fm_fm (x5:x) (fm5:fm) (fm':fm).

Inductive claim : Type :=  (*r claim *)
 | claim_judgment_proof (judgment5:judgment) (proof5:proof).

Definition G : Type := Map.t dyadicfm.
(** induction principles *)
Section t_rect.

Variables
  (P_t : t -> Prop)
  (P_list_t : list t -> Prop).

Hypothesis
  (H_t_var : forall (x5:x), P_t (t_var x5))
  (H_t_const : forall (c5:c), P_t (t_const c5))
  (H_t_func : forall (t_list:list t), P_list_t t_list -> forall (f5:f), P_t (t_func f5 t_list))
  (H_list_t_nil : P_list_t nil)
  (H_list_t_cons : forall (t0:t), P_t t0 -> forall (t_l:list t), P_list_t t_l -> P_list_t (cons t0 t_l)).

Fixpoint t_ott_ind (n:t) : P_t n :=
  match n as x return P_t x with
  | (t_var x5) => H_t_var x5
  | (t_const c5) => H_t_const c5
  | (t_func f5 t_list) => H_t_func t_list (((fix t_list_ott_ind (t_l:list t) : P_list_t t_l := match t_l as x return P_list_t x with nil => H_list_t_nil | cons t1 xl => H_list_t_cons t1(t_ott_ind t1)xl (t_list_ott_ind xl) end)) t_list) f5
end.

End t_rect.


Section entry_proof_rect.

Variables
  (P_entry : entry -> Prop)
  (P_proof : proof -> Prop)
  (P_list_entry : list entry -> Prop).

Hypothesis
  (H_entry_derivation : forall (derivation5:derivation), P_entry (entry_derivation derivation5))
  (H_entry_box : forall (proof5:proof), P_proof proof5 -> P_entry (entry_box proof5))
  (H_entry_invalid : P_entry entry_invalid)
  (H_proof_entries : forall (entry_list:list entry), P_list_entry entry_list -> P_proof (proof_entries entry_list))
  (H_list_entry_nil : P_list_entry nil)
  (H_list_entry_cons : forall (entry0:entry), P_entry entry0 -> forall (entry_l:list entry), P_list_entry entry_l -> P_list_entry (cons entry0 entry_l)).

Fixpoint proof_ott_ind (n:proof) : P_proof n :=
  match n as x return P_proof x with
  | (proof_entries entry_list) => H_proof_entries entry_list (((fix entry_list_ott_ind (entry_l:list entry) : P_list_entry entry_l := match entry_l as x return P_list_entry x with nil => H_list_entry_nil | cons entry1 xl => H_list_entry_cons entry1(entry_ott_ind entry1)xl (entry_list_ott_ind xl) end)) entry_list)
end
with entry_ott_ind (n:entry) : P_entry n :=
  match n as x return P_entry x with
  | (entry_derivation derivation5) => H_entry_derivation derivation5
  | (entry_box proof5) => H_entry_box proof5 (proof_ott_ind proof5)
  | entry_invalid => H_entry_invalid 
end.

End entry_proof_rect.
(** library functions *)
Fixpoint list_mem A (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list A) {struct l} : bool :=
  match l with
  | nil => false
  | cons h t => if eq h x then true else list_mem A eq x t
end.
Implicit Arguments list_mem.


(** substitutions *)
Fixpoint tsubst_t (t_5:t) (x_6:x) (t__6:t) {struct t__6} : t :=
  match t__6 with
  | (t_var x5) => (if eq_x x5 x_6 then t_5 else (t_var x5))
  | (t_const c5) => t_const c5
  | (t_func f5 t_list) => t_func f5 (map (fun (t_:t) => (tsubst_t t_5 x_6 t_)) t_list)
end.

Fixpoint tsubst_fm (t_6:t) (x_6:x) (fm_6:fm) {struct fm_6} : fm :=
  match fm_6 with
  | (fm_pred P5 t_list) => fm_pred P5 (map (fun (t_:t) => (tsubst_t t_6 x_6 t_)) t_list)
  | (fm_eq t5 t') => fm_eq (tsubst_t t_6 x_6 t5) (tsubst_t t_6 x_6 t')
  | (fm_neg fm5) => fm_neg (tsubst_fm t_6 x_6 fm5)
  | (fm_and fm5 fm') => fm_and (tsubst_fm t_6 x_6 fm5) (tsubst_fm t_6 x_6 fm')
  | (fm_or fm5 fm') => fm_or (tsubst_fm t_6 x_6 fm5) (tsubst_fm t_6 x_6 fm')
  | (fm_imp fm5 fm') => fm_imp (tsubst_fm t_6 x_6 fm5) (tsubst_fm t_6 x_6 fm')
  | (fm_forall x5 fm5) => fm_forall x5 (if list_mem eq_x x_6 (cons x5 nil) then fm5 else (tsubst_fm t_6 x_6 fm5))
  | (fm_ex x5 fm5) => fm_ex x5 (if list_mem eq_x x_6 (cons x5 nil) then fm5 else (tsubst_fm t_6 x_6 fm5))
  | fm_cont => fm_cont 
end.

Definition tsubst_derivation (t5:t) (x_6:x) (derivation5:derivation) : derivation :=
  match derivation5 with
  | (derivation_deriv l5 fm5 reason5) => derivation_deriv l5 (tsubst_fm t5 x_6 fm5) reason5
  | (derivation_var l5 x5) => derivation_var l5 x5
  | (derivation_var_assumption l5 x5 fm5) => derivation_var_assumption l5 x5 (tsubst_fm t5 x_6 fm5)
end.

Definition tsubst_fmlist (t5:t) (x5:x) (fmlist5:fmlist) : fmlist :=
  match fmlist5 with
  | (fmlist_list fm_list) => fmlist_list (map (fun (fm_:fm) => (tsubst_fm t5 x5 fm_)) fm_list)
end.

Fixpoint tsubst_entry (t5:t) (x5:x) (entry5:entry) {struct entry5} : entry :=
  match entry5 with
  | (entry_derivation derivation5) => entry_derivation (tsubst_derivation t5 x5 derivation5)
  | (entry_box proof5) => entry_box (tsubst_proof t5 x5 proof5)
  | entry_invalid => entry_invalid 
end
with tsubst_proof (t5:t) (x5:x) (proof_6:proof) {struct proof_6} : proof :=
  match proof_6 with
  | (proof_entries entry_list) => proof_entries (map (fun (entry_:entry) => (tsubst_entry t5 x5 entry_)) entry_list)
end.

Definition tsubst_judgment (t5:t) (x5:x) (judgment5:judgment) : judgment :=
  match judgment5 with
  | (judgment_follows fmlist5 fm5) => judgment_follows (tsubst_fmlist t5 x5 fmlist5) (tsubst_fm t5 x5 fm5)
end.

Definition tsubst_dyadicfm (t5:t) (x_6:x) (dyadicfm5:dyadicfm) : dyadicfm :=
  match dyadicfm5 with
  | (dyadicfm_fm fm5) => dyadicfm_fm (tsubst_fm t5 x_6 fm5)
  | (dyadicfm_fm_fm fm5 fm') => dyadicfm_fm_fm (tsubst_fm t5 x_6 fm5) (tsubst_fm t5 x_6 fm')
  | (dyadicfm_var_fm x5 fm5) => dyadicfm_var_fm x5 (tsubst_fm t5 x_6 fm5)
  | (dyadicfm_var_fm_fm x5 fm5 fm') => dyadicfm_var_fm_fm x5 (tsubst_fm t5 x_6 fm5) (tsubst_fm t5 x_6 fm')
end.

Definition tsubst_claim (t5:t) (x5:x) (claim5:claim) : claim :=
  match claim5 with
  | (claim_judgment_proof judgment5 proof5) => claim_judgment_proof (tsubst_judgment t5 x5 judgment5) (tsubst_proof t5 x5 proof5)
end.

(** library functions *)
Fixpoint list_minus A (eq:forall a b:A,{a=b}+{a<>b}) (l1:list A) (l2:list A) {struct l1} : list A :=
  match l1 with
  | nil => nil
  | cons h t => if (list_mem (A:=A) eq h l2) then list_minus A eq t l2 else cons h (list_minus A eq t l2)
end.
Implicit Arguments list_minus.


(** free variables *)
Fixpoint ftx_t (t_5:t) : list x :=
  match t_5 with
  | (t_var x5) => (cons x5 nil)
  | (t_const c5) => nil
  | (t_func f5 t_list) => ((flat_map (fun (t_:t) => (ftx_t t_)) t_list))
end.

Fixpoint ftx_fm (fm_6:fm) : list x :=
  match fm_6 with
  | (fm_pred P5 t_list) => ((flat_map (fun (t_:t) => (ftx_t t_)) t_list))
  | (fm_eq t5 t') => (app (ftx_t t5) (ftx_t t'))
  | (fm_neg fm5) => ((ftx_fm fm5))
  | (fm_and fm5 fm') => (app (ftx_fm fm5) (ftx_fm fm'))
  | (fm_or fm5 fm') => (app (ftx_fm fm5) (ftx_fm fm'))
  | (fm_imp fm5 fm') => (app (ftx_fm fm5) (ftx_fm fm'))
  | (fm_forall x5 fm5) => ((list_minus eq_x (ftx_fm fm5) (cons x5 nil)))
  | (fm_ex x5 fm5) => ((list_minus eq_x (ftx_fm fm5) (cons x5 nil)))
  | fm_cont => nil
end.

Definition ftx_derivation (derivation5:derivation) : list x :=
  match derivation5 with
  | (derivation_deriv l5 fm5 reason5) => ((ftx_fm fm5))
  | (derivation_var l5 x5) => nil
  | (derivation_var_assumption l5 x5 fm5) => ((ftx_fm fm5))
end.

Definition ftx_fmlist (fmlist5:fmlist) : list x :=
  match fmlist5 with
  | (fmlist_list fm_list) => ((flat_map (fun (fm_:fm) => (ftx_fm fm_)) fm_list))
end.

Fixpoint ftx_entry (entry5:entry) : list x :=
  match entry5 with
  | (entry_derivation derivation5) => ((ftx_derivation derivation5))
  | (entry_box proof5) => ((ftx_proof proof5))
  | entry_invalid => nil
end
with ftx_proof (proof_6:proof) : list x :=
  match proof_6 with
  | (proof_entries entry_list) => ((flat_map (fun (entry_:entry) => (ftx_entry entry_)) entry_list))
end.

Definition ftx_judgment (judgment5:judgment) : list x :=
  match judgment5 with
  | (judgment_follows fmlist5 fm5) => (app (ftx_fmlist fmlist5) (ftx_fm fm5))
end.

Definition ftx_dyadicfm (dyadicfm5:dyadicfm) : list x :=
  match dyadicfm5 with
  | (dyadicfm_fm fm5) => ((ftx_fm fm5))
  | (dyadicfm_fm_fm fm5 fm') => (app (ftx_fm fm5) (ftx_fm fm'))
  | (dyadicfm_var_fm x5 fm5) => ((ftx_fm fm5))
  | (dyadicfm_var_fm_fm x5 fm5 fm') => (app (ftx_fm fm5) (ftx_fm fm'))
end.

Definition ftx_claim (claim5:claim) : list x :=
  match claim5 with
  | (claim_judgment_proof judgment5 proof5) => (app (ftx_judgment judgment5) (ftx_proof proof5))
end.

Definition proof_list_entry (proof5 : proof) : list entry :=
match proof5 with 
| proof_entries ls => ls
end. 

Definition fmlist_list_fm (fmlist5 : fmlist) : list fm :=
match fmlist5 with
| fmlist_list ls => ls
end.

(** definitions *)

(* defns validity *)
Inductive valid_claim : claim -> Prop :=    (* defn valid_claim *)
 | vc_claim : forall (fmlist5:fmlist) (fm5:fm) (proof5:proof) (l5:l) (justification5:justification),
       (last (proof_list_entry  proof5 ) entry_invalid)   =  (entry_derivation (derivation_deriv l5 fm5 (reason_justification justification5)))  ->
     valid_proof  (Map.empty dyadicfm)  fmlist5 proof5 ->
     valid_claim (claim_judgment_proof (judgment_follows fmlist5 fm5) proof5)
with valid_proof : G -> fmlist -> proof -> Prop :=    (* defn valid_proof *)
 | vp_empty : forall (G5:G) (fmlist5:fmlist),
     valid_proof G5 fmlist5  (proof_entries nil) 
 | vp_derivation : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (justification5:justification) (proof5:proof),
     valid_derivation G5 fmlist5 (derivation_deriv l5 fm5 (reason_justification justification5)) ->
     valid_proof  (Map.add (inl  l5 ) (dyadicfm_fm  fm5 )  G5 )  fmlist5 proof5 ->
     valid_proof G5 fmlist5  (proof_entries (cons  (entry_derivation (derivation_deriv l5 fm5 (reason_justification justification5)))  (proof_list_entry  proof5 ))) 
 | vp_box_imp : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (proof5 proof':proof) (l':l) (fm':fm) (reason5:reason),
       (last (proof_list_entry   (proof_entries (cons  (entry_derivation (derivation_deriv l5 fm5 reason_assumption))  (proof_list_entry  proof5 )))  ) entry_invalid)   =  (entry_derivation (derivation_deriv l' fm' reason5))  ->
     valid_proof  (Map.add (inl  l5 ) (dyadicfm_fm  fm5 )  G5 )  fmlist5 proof5 ->
     valid_proof  (Map.add (inr ( l5 ,  l' )) (dyadicfm_fm_fm  fm5   fm' )  G5 )  fmlist5 proof' ->
     valid_proof G5 fmlist5  (proof_entries (cons  (entry_box  (proof_entries (cons  (entry_derivation (derivation_deriv l5 fm5 reason_assumption))  (proof_list_entry  proof5 ))) )  (proof_list_entry  proof' ))) 
 | vp_box_all : forall (G5:G) (fmlist5:fmlist) (l5:l) (x5:x) (proof5 proof':proof) (l':l) (fm':fm) (reason5:reason),
       (last (proof_list_entry  proof5 ) entry_invalid)   =  (entry_derivation (derivation_deriv l' fm' reason5))  ->
     valid_proof G5 fmlist5 proof5 ->
     valid_proof  (Map.add (inr ( l5 ,  l' )) (dyadicfm_var_fm  x5   fm' )  G5 )  fmlist5 proof' ->
     valid_proof G5 fmlist5  (proof_entries (cons  (entry_box  (proof_entries (cons  (entry_derivation (derivation_var l5 x5))  (proof_list_entry  proof5 ))) )  (proof_list_entry  proof' ))) 
 | vp_box_ex : forall (G5:G) (fmlist5:fmlist) (l5:l) (x5:x) (fm5:fm) (proof5 proof':proof) (l':l) (fm':fm) (reason5:reason),
       (last (proof_list_entry  proof5 ) entry_invalid)   =  (entry_derivation (derivation_deriv l' fm' reason5))  ->
     valid_proof  (Map.add (inl  l5 ) (dyadicfm_fm  fm5 )  G5 )  fmlist5 proof5 ->
     valid_proof  (Map.add (inr ( l5 ,  l' )) (dyadicfm_var_fm_fm  x5   fm5   fm' )  G5 )  fmlist5 proof' ->
     valid_proof G5 fmlist5  (proof_entries (cons  (entry_box  (proof_entries (cons  (entry_derivation (derivation_var_assumption l5 x5 fm5))  (proof_list_entry  proof5 ))) )  (proof_list_entry  proof' ))) 
with valid_derivation : G -> fmlist -> derivation -> Prop :=    (* defn valid_derivation *)
 | vd_premise : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm),
      (In  fm5  (fmlist_list_fm  fmlist5 ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 fm5 (reason_justification justification_premise))
 | vd_lem : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm),
     valid_derivation G5 fmlist5 (derivation_deriv l5 (fm_or fm5 (fm_neg fm5)) (reason_justification justification_lem))
 | vd_copy : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (l':l),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  fm5 ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 fm5 (reason_justification (justification_copy l')))
 | vd_conte : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (l':l),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  fm_cont ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 fm5 (reason_justification (justification_conte l')))
 | vd_andi : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm5 fm':fm) (l1 l2:l),
      (Map.find (inl  l1 )  G5  = Some (dyadicfm_fm  fm5 ))  ->
      (Map.find (inl  l2 )  G5  = Some (dyadicfm_fm  fm' ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 (fm_and fm5 fm') (reason_justification (justification_andi l1 l2)))
 | vd_ande1 : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (l':l) (fm':fm),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  (fm_and fm5 fm') ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 fm5 (reason_justification (justification_ande1 l')))
 | vd_ande2 : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm':fm) (l':l) (fm5:fm),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  (fm_and fm5 fm') ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 fm' (reason_justification (justification_ande2 l')))
 | vd_ori1 : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5 fm':fm) (l':l),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  fm5 ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 (fm_or fm5 fm') (reason_justification (justification_ori1 l')))
 | vd_ori2 : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5 fm':fm) (l':l),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  fm' ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 (fm_or fm5 fm') (reason_justification (justification_ori2 l')))
 | vd_impe : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm5:fm) (l1 l2:l) (fm':fm),
      (Map.find (inl  l1 )  G5  = Some (dyadicfm_fm  fm' ))  ->
      (Map.find (inl  l2 )  G5  = Some (dyadicfm_fm  (fm_imp fm' fm5) ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 fm5 (reason_justification (justification_impe l1 l2)))
 | vd_negnegi : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (l':l),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  fm5 ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 (fm_neg (fm_neg fm5)) (reason_justification (justification_negnegi l')))
 | vd_negnege : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (l':l),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  (fm_neg (fm_neg fm5)) ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 fm5 (reason_justification (justification_negnege l')))
 | vd_mt : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm5:fm) (l1 l2:l) (fm':fm),
      (Map.find (inl  l1 )  G5  = Some (dyadicfm_fm  (fm_imp fm5 fm') ))  ->
      (Map.find (inl  l2 )  G5  = Some (dyadicfm_fm  (fm_neg fm') ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 (fm_neg fm5) (reason_justification (justification_mt l1 l2)))
 | vd_nege : forall (G5:G) (fmlist5:fmlist) (l_5 l1 l2:l) (fm5:fm),
      (Map.find (inl  l1 )  G5  = Some (dyadicfm_fm  fm5 ))  ->
      (Map.find (inl  l2 )  G5  = Some (dyadicfm_fm  (fm_neg fm5) ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 fm_cont (reason_justification (justification_nege l1 l2)))
 | vd_impi : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm5 fm':fm) (l1 l2:l),
      (Map.find (inr ( l1 ,  l2 ))  G5  = Some (dyadicfm_fm_fm  fm5   fm' ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 (fm_imp fm5 fm') (reason_justification (justification_impi l1 l2)))
 | vd_negi : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm5:fm) (l1 l2:l),
      (Map.find (inr ( l1 ,  l2 ))  G5  = Some (dyadicfm_fm_fm  fm5   fm_cont ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 (fm_neg fm5) (reason_justification (justification_negi l1 l2)))
 | vd_ore : forall (G5:G) (fmlist5:fmlist) (l_6:l) (fm'':fm) (l1 l2 l3 l4 l5:l) (fm5 fm':fm),
      (Map.find (inl  l1 )  G5  = Some (dyadicfm_fm  (fm_or fm5 fm') ))  ->
      (Map.find (inr ( l2 ,  l3 ))  G5  = Some (dyadicfm_fm_fm  fm5   fm'' ))  ->
      (Map.find (inr ( l4 ,  l5 ))  G5  = Some (dyadicfm_fm_fm  fm'   fm'' ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_6 fm'' (reason_justification (justification_ore l1 l2 l3 l4 l5)))
 | vd_pbc : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm5:fm) (l1 l2:l),
      (Map.find (inr ( l1 ,  l2 ))  G5  = Some (dyadicfm_fm_fm  (fm_neg fm5)   fm_cont ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 fm5 (reason_justification (justification_pbc l1 l2)))
 | vd_eqi : forall (G5:G) (fmlist5:fmlist) (l5:l) (t5:t),
     valid_derivation G5 fmlist5 (derivation_deriv l5 (fm_eq t5 t5) (reason_justification justification_eqi))
 | vd_eqe : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm5:fm) (t':t) (x5:x) (l1 l2:l) (t5:t),
      (Map.find (inl  l1 )  G5  = Some (dyadicfm_fm  (fm_eq t5 t') ))  ->
      (Map.find (inl  l2 )  G5  = Some (dyadicfm_fm   (tsubst_fm  t5   x5   fm5 )  ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5  (tsubst_fm  t'   x5   fm5 )  (reason_justification (justification_eqe l1 l2)))
 | vd_alle : forall (G5:G) (fmlist5:fmlist) (l5:l) (fm5:fm) (t5:t) (x5:x) (l':l),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm  (fm_forall x5 fm5) ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5  (tsubst_fm  t5   x5   fm5 )  (reason_justification (justification_alle l')))
 | vd_exi : forall (G5:G) (fmlist5:fmlist) (l5:l) (x5:x) (fm5:fm) (l':l) (t5:t),
      (Map.find (inl  l' )  G5  = Some (dyadicfm_fm   (tsubst_fm  t5   x5   fm5 )  ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l5 (fm_ex x5 fm5) (reason_justification (justification_exi l')))
 | vd_alli : forall (G5:G) (fmlist5:fmlist) (l_5:l) (x5:x) (fm5:fm) (l1 l2:l) (x':x),
      (Map.find (inr ( l1 ,  l2 ))  G5  = Some (dyadicfm_var_fm  x'    (tsubst_fm  (t_var x')   x5   fm5 )  ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 (fm_forall x5 fm5) (reason_justification (justification_alli l1 l2)))
 | vd_exe : forall (G5:G) (fmlist5:fmlist) (l_5:l) (fm':fm) (l1 l2 l3:l) (x5:x) (fm5:fm) (x':x),
      (Map.find (inl  l1 )  G5  = Some (dyadicfm_fm  (fm_ex x5 fm5) ))  ->
      (Map.find (inr ( l2 ,  l3 ))  G5  = Some (dyadicfm_var_fm_fm  x'    (tsubst_fm  (t_var x')   x5   fm5 )    fm' ))  ->
     valid_derivation G5 fmlist5 (derivation_deriv l_5 fm' (reason_justification (justification_exe l1 l2 l3))).
End FitchFirstOrder.