module Types

  use Functions.Func
  use Firstorder_term_spec.Spec

  (* The prover return a contradictory assignment.
     To be perfectly correct, its initial
     input (even before preprocessing) should not
     contain any free variable of kind term. *)

  type prover_return = {
    ghost contradictory_assignment : int -> (fo_term int int) ;
  }

end

module Logic

  use FormulaTransformations.Types
  use FormulaTransformations.Logic
  use Firstorder_formula_list_spec.Spec
  use Firstorder_formula_spec.Spec
  use Firstorder_symbol_spec.Spec
  use Firstorder_term_spec.Spec
  use Firstorder_tableau_spec.Spec
  use Functions.Func
  use bool.Bool
  use Firstorder_semantics.Sem

  predicate is_atom_list (phil:fo_formula_list 'ls 'b) = match phil with
    | FOFNil -> true
    | FOFCons x q -> is_atom x /\ is_atom_list q
  end

  let lemma is_atom_subst (phi:fo_formula 'ls 'b)
    (sigma:'b -> (fo_term 'ls 'c)) : unit
    requires { is_atom phi }
    ensures { is_atom (subst_fo_formula phi subst_id_symbol sigma) }
  =
    match phi with
      | PApp _ _ -> ()
      | Not (PApp _ _ ) -> ()
      | _ -> absurd
    end

  let rec lemma is_atom_list_subst (phil:fo_formula_list 'ls 'b)
    (sigma:'b -> (fo_term 'ls 'c)) : unit
    requires { is_atom_list phil }
    ensures { is_atom_list (subst_fo_formula_list phil subst_id_symbol sigma) }
    variant { size_fo_formula_list phil }
  =
    match phil with
      | FOFNil -> ()
      | FOFCons x q -> is_atom_list_subst q sigma
    end

  predicate is_procedure_tableau (t:tableau 'ls 'b) = match t with
    | Root -> true
    | Node tnext phi0 phib -> is_procedure_tableau tnext /\
      is_atom phi0 /\ is_atom_list phib
  end

  let rec lemma is_procedure_tableau_subst (t:tableau 'ls 'b)
    (sigma:'b -> (fo_term 'ls 'c)) : unit
    requires { is_procedure_tableau t }
    ensures { is_procedure_tableau (subst_tableau t subst_id_symbol sigma) }
    variant { size_tableau t }
  =
    match t with
      | Root -> ()
      | Node tnext phi0 phib -> is_procedure_tableau_subst tnext sigma
    end

  (*let rec lemma tableau_semantic_increasing (t:tableau 'ls 'b)
    (b1 b2:bool) (m:model 'ls 'st) (rho:'b -> 'st) : unit
    requires { implb b1 b2 = True }
    ensures { tableau_semantic_with t b1 m rho ->
      tableau_semantic_with t b2 m rho }
    variant { size_tableau t }
  =
    match t with
      | Root -> ()
      | Node tnext phi0 phib ->
        tableau_semantic_increasing tnext (tableau_node b1 phib phi0 m rho)
          (tableau_node b2 phib phi0 m rho) m rho
    end*)

end

module Impl

  use Firstorder_semantics.Sem
  use Firstorder_symbol_spec.Spec
  use Firstorder_symbol_impl.Types
  use Firstorder_symbol_impl.Logic
  use Firstorder_symbol_impl.Impl
  use Firstorder_term_spec.Spec
  use Firstorder_term_impl.Types
  use Firstorder_term_impl.Logic
  use Firstorder_term_impl.Impl
  use Firstorder_formula_spec.Spec
  use Firstorder_formula_impl.Types
  use Firstorder_formula_impl.Logic
  use Firstorder_formula_impl.Impl
  use Firstorder_formula_list_spec.Spec
  use Firstorder_formula_list_impl.Types
  use Firstorder_formula_list_impl.Logic
  use Firstorder_formula_list_impl.Impl
  use Firstorder_tableau_spec.Spec
  use Firstorder_tableau_impl.Types
  use Firstorder_tableau_impl.Logic
  use Firstorder_tableau_impl.Impl
  use FormulaTransformations.Types
  use FormulaTransformations.Logic
  use FormulaTransformations.Impl
  use Unification.Types
  use Unification.Logic
  use Unification.Impl
  use BacktrackArray.Logic
  use BacktrackArray.Impl
  use Functions.Func
  use option.Option
  use OptionFuncs.Funcs
  use bool.Bool
  use int.Int
  use Types
  use Logic
  use ref.Ref
  use list.List

  exception Failure

  let rec merge (phi1 phi2:nlimpl_fo_formula_list) (ghost st:'st) : nlimpl_fo_formula_list
    requires { nlimpl_fo_formula_list_ok phi1 }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      phi1.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok phi2 }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      phi2.model_fo_formula_list_field -> x >= 0 }
    requires { is_atom_list phi1.model_fo_formula_list_field }
    requires { is_atom_list phi2.model_fo_formula_list_field }
    ensures { nlimpl_fo_formula_list_ok result }
    ensures { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      result.model_fo_formula_list_field -> x >= 0 }
    ensures { forall m:model int 'st,rho:int -> 'st.
      formula_list_disj_semantic result.model_fo_formula_list_field m rho <->
        formula_list_disj_semantic phi1.model_fo_formula_list_field m rho \/
        formula_list_disj_semantic phi2.model_fo_formula_list_field m rho }
    ensures { is_atom_list result.model_fo_formula_list_field }
    variant { size_fo_formula_list phi1.model_fo_formula_list_field }
  =
    let phi1m = phi1.model_fo_formula_list_field in
    let phi2m = phi2.model_fo_formula_list_field in
    match destruct_fo_formula_list phi1 with
      | NLC_FOFNil -> phi2
      | NLC_FOFCons phi0 q ->
        let phi0m = phi0.model_fo_formula_field in
        let qm = q.model_fo_formula_list_field in
        assert { phi1m = FOFCons phi0m qm } ;
        let phi3 = construct_fo_formula_list (NLC_FOFCons phi0 phi2) in
        let phi3m = phi3.model_fo_formula_list_field in
        assert { phi3m = FOFCons phi0m phi2m } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi0m ->
          is_fo_term_free_var_in_fo_formula_list x phi1m && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phi3m ->
          (is_fo_term_free_var_in_fo_formula x phi0m \/
           is_fo_term_free_var_in_fo_formula_list x phi2m) && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x qm ->
          is_fo_term_free_var_in_fo_formula_list x phi1m && x >= 0 } ;
        merge q phi3 st
    end

  (* extend the current tableau branch by the given formula list.
     equivalent to contraction of empty branches
     until a non-empty branch is found. *)
  let rec contract_tableau (tab:nlimpl_tableau)
    (branch:nlimpl_fo_formula_list) (ndepth:ref int) (ghost st:'st) : option nlimpl_tableau
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok branch }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      branch.model_fo_formula_list_field -> x >= 0 }
    requires { is_procedure_tableau tab.model_tableau_field }
    requires { is_atom_list branch.model_fo_formula_list_field }
    returns { None -> forall m:model int 'st,rho:int -> 'st.
        let b = if formula_list_disj_semantic branch.model_fo_formula_list_field m rho
          then True
          else False in
        not(tableau_semantic_with tab.model_tableau_field b m rho)
      | Some x -> (forall m:model int 'st,rho:int -> 'st.
        let b = if formula_list_disj_semantic branch.model_fo_formula_list_field m rho
          then True
          else False in
        tableau_semantic_with tab.model_tableau_field b m rho ->
          tableau_semantic_with x.model_tableau_field True m rho) /\
        is_procedure_tableau x.model_tableau_field /\
        nlimpl_tableau_ok x /\
        (forall y:int. is_fo_term_free_var_in_tableau y x.model_tableau_field
          -> y >= 0) }
    variant { size_tableau tab.model_tableau_field }
  =
    let tabm = tab.model_tableau_field in
    let brm = branch.model_fo_formula_list_field in
    match destruct_fo_formula_list branch with
      | NLC_FOFNil -> assert { brm = FOFNil } ;
        assert { forall m:model int 'st,rho:int -> 'st.
              not(formula_list_disj_semantic brm m rho) } ;
        match destruct_tableau tab with
          | NLC_Root -> assert { tabm = Root } ; None
          | NLC_Node tnext phi0 phib ->
            let tnm = tnext.model_tableau_field in
            let phi0m = phi0.model_fo_formula_field in
            let phibm = phib.model_fo_formula_list_field in
            assert { tabm = Node tnm phi0m phibm } ;
            assert { forall x:int. is_fo_term_free_var_in_tableau x tnm ->
              is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
            assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phibm ->
              is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
            assert { forall m:model int 'st,rho:int -> 'st.
              tableau_semantic_with tab.model_tableau_field False m rho ->
              let b = if formula_list_disj_semantic phibm m rho
                then True
                else False in
              tableau_semantic_with tnm b m rho } ;
            ndepth := !ndepth + 1 ;
            contract_tableau tnext phib ndepth st
        end
      | NLC_FOFCons phi0 qb -> let phi0m = phi0.model_fo_formula_field in
        let qbm = qb.model_fo_formula_list_field in
        assert { brm = FOFCons phi0m qbm } ;
        let ftab = construct_tableau (NLC_Node tab phi0 qb) in
        let ftabm = ftab.model_tableau_field in
        assert { ftabm = Node tabm phi0m qbm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi0m ->
          is_fo_term_free_var_in_fo_formula_list x brm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x qbm ->
          is_fo_term_free_var_in_fo_formula_list x brm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_tableau x ftabm ->
          (is_fo_term_free_var_in_tableau x tabm
            \/ is_fo_term_free_var_in_fo_formula x phi0m
            \/ is_fo_term_free_var_in_fo_formula_list x qbm) && x >= 0 } ;
        Some ftab
    end

  let rec branch_conflict_atom (p1:int) (t1:nlimpl_fo_term_list) (tab:nlimpl_tableau)
    (rhob:subst) (ghost rho:unifier_subst) : unit
    requires { nlimpl_fo_term_list_ok t1 }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t1.model_fo_term_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok rhob rho }
    requires { is_procedure_tableau tab.model_tableau_field }
    ensures { precede (old rhob) rhob }
    ensures { unifier_subst_ok rhob rho }
    raises { Failure -> precede (old rhob) rhob /\ correct rhob }
    diverges (* variant { size_tableau tab.model_tableau_field } *)
  =
    let tabm = tab.model_tableau_field in
    match destruct_tableau tab with
      | NLC_Root -> ()
      | NLC_Node tnext phi1 phib ->
        let tnextm = tnext.model_tableau_field in
        let phi1m = phi1.model_fo_formula_field in
        let phibm = phib.model_fo_formula_list_field in
        assert { tabm = Node tnextm phi1m phibm } ;
        assert { is_atom phi1m } ;
        assert { forall x:int. is_fo_term_free_var_in_tableau x tnextm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        match destruct_fo_formula phi1 with
          | NLC_PApp p2 t2 -> let p2m = p2.model_symbol_field in
            let t2m = t2.model_fo_term_list_field in
            assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t2m ->
              is_fo_term_free_var_in_fo_formula x phi1m &&
              is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
            let p3 = match destruct_symbol p2 with
              | NLCVar_symbol p3 -> p3 end in
            if p1 = p3
            then begin
              try conflict t1 t2 rhob rho with UnificationFailure ->
              raise Failure end ;
              branch_conflict_atom p1 t1 tnext rhob rho
            end
            else branch_conflict_atom p1 t1 tnext rhob rho
          | NLC_Not _ -> branch_conflict_atom p1 t1 tnext rhob rho
          | _ -> absurd
        end
    end

  let rec branch_conflict_neg_atom (p1:int) (t1:nlimpl_fo_term_list) (tab:nlimpl_tableau)
    (rhob:subst) (ghost rho:unifier_subst) : unit
    requires { nlimpl_fo_term_list_ok t1 }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t1.model_fo_term_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok rhob rho }
    requires { is_procedure_tableau tab.model_tableau_field }
    ensures { precede (old rhob) rhob }
    ensures { unifier_subst_ok rhob rho }
    raises { Failure -> precede (old rhob) rhob /\ correct rhob }
    diverges (* variant { size_tableau tab.model_tableau_field } *)
  =
    let tabm = tab.model_tableau_field in
    match destruct_tableau tab with
      | NLC_Root -> ()
      | NLC_Node tnext phi1 phib ->
        let tnextm = tnext.model_tableau_field in
        let phi1m = phi1.model_fo_formula_field in
        let phibm = phib.model_fo_formula_list_field in
        assert { tabm = Node tnextm phi1m phibm } ;
        assert { is_atom phi1m } ;
        assert { forall x:int. is_fo_term_free_var_in_tableau x tnextm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        match destruct_fo_formula phi1 with
          | NLC_Not phi2 -> let phi2m = phi2.model_fo_formula_field in
            assert { phi1m = Not phi2m } ;
            match destruct_fo_formula phi2 with
              | NLC_PApp p2 t2 -> let p2m = p2.model_symbol_field in
                let t2m = t2.model_fo_term_list_field in
                assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t2m ->
                  is_fo_term_free_var_in_fo_formula x phi1m &&
                  is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
                let p3 = match destruct_symbol p2 with
                  | NLCVar_symbol p3 -> p3 end in
                if p1 = p3
                then begin
                  try conflict t1 t2 rhob rho with UnificationFailure ->
                  raise Failure end ;
                  branch_conflict_atom p1 t1 tnext rhob rho
                end
                else branch_conflict_atom p1 t1 tnext rhob rho
              | _ -> absurd
            end
          | NLC_PApp _ _ -> branch_conflict_atom p1 t1 tnext rhob rho
          | _ -> absurd
        end
    end

  let rec clause_conflicts (phil:nlimpl_fo_formula_list) (tab:nlimpl_tableau)
    (rhob:subst) (ghost rho:unifier_subst) : unit
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      phil.model_fo_formula_list_field -> x >= 0 }
    requires { is_atom_list phil.model_fo_formula_list_field }
    requires { nlimpl_fo_formula_list_ok phil }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { is_procedure_tableau tab.model_tableau_field }
    requires { nlimpl_tableau_ok tab }
    requires { unifier_subst_ok rhob rho }
    ensures { precede (old rhob) rhob }
    ensures { unifier_subst_ok rhob rho }
    raises { Failure -> precede (old rhob) rhob /\ correct rhob }
    diverges (* variant { size_fo_formula_list phil.model_fo_formula_list_field } *)
  =
    let philm = phil.model_fo_formula_list_field in
    match destruct_fo_formula_list phil with
      | NLC_FOFNil -> ()
      | NLC_FOFCons phi0 phiq -> let phi0m = phi0.model_fo_formula_field in
        let phiqm = phiq.model_fo_formula_list_field in
        assert { philm = FOFCons phi0m phiqm } ;
        assert { is_atom phi0m } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phiqm ->
          is_fo_term_free_var_in_fo_formula_list x philm && x >= 0 } ;
        match destruct_fo_formula phi0 with
          | NLC_PApp p1 t1 -> let p1m = p1.model_symbol_field in
            let t1m = t1.model_fo_term_list_field in
            assert { phi0m = PApp p1m t1m } ;
            let p1' = match destruct_symbol p1 with
              | NLCVar_symbol p1' -> p1'
            end in
            assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t1m ->
              is_fo_term_free_var_in_fo_formula x phi0m &&
              is_fo_term_free_var_in_fo_formula_list x philm && x >= 0 } ;
            branch_conflict_atom p1' t1 tab rhob rho ;
            clause_conflicts phiq tab rhob rho
          | NLC_Not phi1 -> let phi1m = phi1.model_fo_formula_field in
            assert { phi0m = Not phi1m } ;
            match destruct_fo_formula phi1 with
              | NLC_PApp p1 t1 -> let p1' = match destruct_symbol p1 with
                  | NLCVar_symbol p1' -> p1'
                end in
                let t1m = t1.model_fo_term_list_field in
                let p1m = p1.model_symbol_field in
                assert { phi1m = PApp p1m t1m } ;
                assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t1m ->
                  is_fo_term_free_var_in_fo_formula x phi1m &&
                  is_fo_term_free_var_in_fo_formula x phi0m &&
                  is_fo_term_free_var_in_fo_formula_list x philm && x >= 0 } ;
                branch_conflict_neg_atom p1' t1 tab rhob rho ;
                clause_conflicts phiq tab rhob rho
              | _ -> absurd
            end
          | _ -> absurd
        end
    end

  (* base:set of initial (preprocessed) formula.
     tab:context still to be proved.
     Return: nothing, if successful, base is unsatisfiable.
     May fail without justification.
   *)

  let rec decompose (base:nlimpl_fo_formula_list)
      (tab:nlimpl_tableau)
      (unifb:subst)
      (ghost unif:unifier_subst)
      (fresh:int)
      (phi0:nlimpl_fo_formula)
      (clause:nlimpl_fo_formula_list)
      (remaining:nlimpl_fo_formula_list)
      (depth:int)
      (goalnum:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }
    requires { nlimpl_fo_formula_ok phi0 }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula x
      phi0.model_fo_formula_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok clause }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      clause.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok remaining }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      remaining.model_fo_formula_list_field -> x >= 0 }

    requires { is_procedure_tableau tab.model_tableau_field }

    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { is_simpl phi0.model_fo_formula_field }
    requires { no_existential phi0.model_fo_formula_field }
    requires { is_nnf phi0.model_fo_formula_field }

    requires { is_atom_list clause.model_fo_formula_list_field }

    requires { is_simpl_list remaining.model_fo_formula_list_field }
    requires { is_nnf_list remaining.model_fo_formula_list_field }
    requires { no_existential_list remaining.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos }
    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        formula_semantic phi0.model_fo_formula_field m rhos \/
        formula_list_disj_semantic clause.model_fo_formula_list_field m rhos \/
        formula_list_disj_semantic remaining.model_fo_formula_list_field m rhos }
    diverges
    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    let phi0m = phi0.model_fo_formula_field in
    let rmgm = remaining.model_fo_formula_list_field in
    let basem = base.model_fo_formula_list_field in
    let clausem = clause.model_fo_formula_list_field in
    let tabm = tab.model_tableau_field in
    match destruct_fo_formula phi0 with
      | NLC_Or a b ->
        let am = a.model_fo_formula_field in
        let bm = b.model_fo_formula_field in
        assert { phi0m = Or am bm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x am ->
          is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x bm ->
          is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
        let rmg = construct_fo_formula_list (NLC_FOFCons b remaining) in
        let rmg'_m = rmg.model_fo_formula_list_field in
        assert { rmg'_m = FOFCons bm rmgm } ;
        decompose base tab unifb unif fresh a clause rmg depth goalnum st
      | NLC_And a b -> let am = a.model_fo_formula_field in
        let bm = b.model_fo_formula_field in
        assert { phi0m = And am bm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x am ->
          is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x bm ->
          is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
        label B in
        let tp = stamp unifb in
        try decompose base tab unifb unif fresh a clause remaining depth goalnum st
        with Failure -> label F in backtrack tp unifb ;
          assert { backtrack_to (unifb at B) (unifb at F) unifb } ;
          decompose base tab unifb unif fresh b clause remaining depth goalnum st end
      | NLC_Exists _ _ -> absurd
      | NLC_FTrue -> absurd
      | NLC_FFalse -> absurd
      | NLC_Forall x phi1 ->
        let phi1m = phi1.model_fo_formula_field in
        let vfresh = construct_fo_term (NLCVar_fo_term fresh) in
        let phi2 = nlsubst_fo_term_in_fo_formula phi1 x vfresh in
        let phi2m = phi2.model_fo_formula_field in
        let ghost r0 = some[x <- None] in
        let ghost r1 = ocase identity x in
        let ghost r2 = ocase identity fresh in
        let ghost r3 = identity[x <- fresh] in
        let ghost sid = (subst_id_fo_term:int -> (fo_term int int)) in
        let ghost s3 = sid[x <- Var_fo_term fresh] in
        let ghost s3' = rcompose r3 sid in
        let ghost s2 = rcompose r2 sid in
        assert { extensionalEqual s3' s3 } ;
        let ghost phi3m = rename_fo_formula phi1m identity r0 in
        assert { phi0m = Forall phi3m &&
          phi1m = rename_fo_formula phi3m identity r1 } ;
        assert { phi2m = subst_fo_formula phi1m (rcompose identity subst_id_symbol) s3'
          = rename_fo_formula phi1m identity r3 } ;
        assert { extensionalEqual r3 (rcompose r0 r2) } ;
        assert { phi2m = rename_fo_formula phi3m identity r2 =
          subst_fo_formula phi3m subst_id_symbol s2 } ;
        assert { forall m:model int 'st, rho:int -> 'st.
          let rhos = semantic_subst unif.unifier m rho in
          let s0 = semantic_subst s2 m rhos in
          let s1 = ocase rhos (term_semantic (Var_fo_term fresh) m rhos) in
          s0 None = s1 None &&
          (forall x:int. s2 (Some x) = Var_fo_term x &&
            s0 (Some x) = term_semantic (Var_fo_term x) m rhos = s1 (Some x)) &&
          extensionalEqual s0 s1 &&
          (formula_semantic phi0m m rhos ->
            formula_semantic phi2m m rhos)
        } ;
        assert { forall x:int.
          (forall y:option int. is_fo_term_free_var_in_fo_formula y phi3m /\
            r2 y = x -> match y with None -> x = fresh && x >= 0
              | Some y -> x = y &&
                is_fo_term_free_var_in_fo_formula (Some x) phi3m &&
                is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 end &&
              x >= 0) &&
          (is_fo_term_free_var_in_fo_formula x phi2m ->
          (exists y:option int. is_fo_term_free_var_in_fo_formula y phi3m /\
            r2 y = x) && x >= 0) &&
          (is_fo_term_free_var_in_fo_formula x phi2m -> x >= 0)
        } ;
        decompose base tab unifb unif (fresh + 1) phi2 clause remaining depth goalnum st
      | NLC_PApp p l ->  assert { is_atom phi0m } ;
        decompose_literal base tab unifb unif fresh phi0 clause remaining depth goalnum st
      | NLC_Not phi1 -> assert { is_atom phi0m } ;
        decompose_literal base tab unifb unif fresh phi0 clause remaining depth goalnum st
    end

  with decompose_literal (base:nlimpl_fo_formula_list)
      (tab:nlimpl_tableau)
      (unifb:subst)
      (ghost unif:unifier_subst)
      (fresh:int)
      (phi0:nlimpl_fo_formula)
      (clause:nlimpl_fo_formula_list)
      (remaining:nlimpl_fo_formula_list)
      (depth:int)
      (goalnum:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }
    requires { nlimpl_fo_formula_ok phi0 }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula x
      phi0.model_fo_formula_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok clause }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      clause.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok remaining }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      remaining.model_fo_formula_list_field -> x >= 0 }

    requires { is_procedure_tableau tab.model_tableau_field }

    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { is_atom phi0.model_fo_formula_field }

    requires { is_atom_list clause.model_fo_formula_list_field }

    requires { is_simpl_list remaining.model_fo_formula_list_field }
    requires { is_nnf_list remaining.model_fo_formula_list_field }
    requires { no_existential_list remaining.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos }
    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        formula_semantic phi0.model_fo_formula_field m rhos \/
        formula_list_disj_semantic clause.model_fo_formula_list_field m rhos \/
        formula_list_disj_semantic remaining.model_fo_formula_list_field m rhos }

    diverges
    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    let phi0m = phi0.model_fo_formula_field in
    let rmgm = remaining.model_fo_formula_list_field in
    let basem = base.model_fo_formula_list_field in
    let clausem = clause.model_fo_formula_list_field in
    let tabm = tab.model_tableau_field in
    match destruct_fo_formula_list remaining with
      | NLC_FOFNil -> assert { rmgm = FOFNil } ;
        match destruct_tableau tab with
          | NLC_Root -> (* Topmost decomposition,
                do not look for contradiction here. *)
            let tab' = construct_tableau (NLC_Node tab phi0 clause) in
            let tab'_m = tab'.model_tableau_field in
            assert { tab'_m = Node tabm phi0m clausem } ;
            if depth = 0 then raise Failure else
            select_lemma base base tab' unifb unif fresh (depth-1) goalnum (-1) st
          | NLC_Node tnext phi1 phib ->
            let clse = construct_fo_formula_list (NLC_FOFCons phi0 clause) in
            let clsem = clse.model_fo_formula_list_field in
            let phi1m = phi1.model_fo_formula_field in
            let tnextm = tnext.model_tableau_field in
            let phibm = phib.model_fo_formula_list_field in
            assert { clsem = FOFCons phi0m clausem } ;
            assert { is_atom_list clsem } ;
            assert { tabm = Node tnextm phi1m phibm } ;
            assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phibm ->
              is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
            assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi1m ->
              is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
            assert { forall x:int. is_fo_term_free_var_in_tableau x tnextm ->
              is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
            let fonil = construct_fo_formula_list NLC_FOFNil in
            assert { fonil.model_fo_formula_list_field = FOFNil } ;
            assert { is_atom phi1m } ;
            match destruct_fo_formula phi1 with
              | NLC_PApp ptab ttab ->
                let ptabm = ptab.model_symbol_field in
                let ttabm = ttab.model_fo_term_list_field in
                assert { phi1m = PApp ptabm ttabm } ;
                assert { forall x:int. is_fo_term_free_var_in_fo_term_list x ttabm ->
                  is_fo_term_free_var_in_fo_formula x phi1m && x >= 0 } ;
                let ptab2 = match destruct_symbol ptab with
                  | NLCVar_symbol ptab2 -> assert { ptabm = Var_symbol ptab2 } ;
                    ptab2
                end in
                contradiction_atom base tab unifb unif fresh ptab2 ttab phibm tnextm clsem clse fonil depth goalnum st
              | NLC_Not phi2 -> let phi2m = phi2.model_fo_formula_field in
                assert { phi1m = Not phi2m } ;
                assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi2m
                  -> is_fo_term_free_var_in_fo_formula x phi1m && x >= 0 } ;
                match destruct_fo_formula phi2 with
                  | NLC_PApp ptab ttab ->
                    let ptabm = ptab.model_symbol_field in
                    let ttabm = ttab.model_fo_term_list_field in
                    assert { phi2m = PApp ptabm ttabm } ;
                    assert { forall x:int. is_fo_term_free_var_in_fo_term_list x ttabm ->
                      is_fo_term_free_var_in_fo_formula x phi2m && x >= 0 } ;
                    let ptab2 = match destruct_symbol ptab with
                      | NLCVar_symbol ptab2 -> assert { ptabm = Var_symbol ptab2 } ;
                        ptab2
                    end in
                    contradiction_neg_atom base tab unifb unif fresh ptab2 ttab phibm tnextm clsem clse fonil depth goalnum st
                  | _ -> absurd
                end
              | _ -> absurd
            end
        end
      | NLC_FOFCons phi1 qr ->
        let phi1m = phi1.model_fo_formula_field in
        let qrm = qr.model_fo_formula_list_field in
        assert { rmgm = FOFCons phi1m qrm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi1m ->
          is_fo_term_free_var_in_fo_formula_list x rmgm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x qrm ->
          is_fo_term_free_var_in_fo_formula_list x rmgm && x >= 0 } ;
        let clse = construct_fo_formula_list (NLC_FOFCons phi0 clause) in
        let clsem = clse.model_fo_formula_list_field in
        assert { clsem = FOFCons phi0m clausem } ;
        decompose base tab unifb unif fresh phi1 clse qr depth goalnum st
    end

  (* find a contradiction with the current leaf of the tableau,
     if it is a non-negated literal. *)
  with contradiction_atom (base:nlimpl_fo_formula_list)
      (tab:nlimpl_tableau)
      (unifb:subst)
      (ghost unif:unifier_subst)
      (fresh:int)
      (p:int)
      (t:nlimpl_fo_term_list)
      (ghost phit:fo_formula_list int int)
      (ghost tnext:tableau int int)
      (ghost clsem:fo_formula_list int int)
      (phil:nlimpl_fo_formula_list)
      (phiacc:nlimpl_fo_formula_list)
      (depth:int)
      (goalnum:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok phil }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      phil.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok phiacc }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      phiacc.model_fo_formula_list_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }
    requires { nlimpl_fo_term_list_ok t }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t.model_fo_term_list_field -> x >= 0 }

    requires { tab.model_tableau_field =
      Node tnext (PApp (Var_symbol p) t.model_fo_term_list_field) phit }

    requires { is_procedure_tableau tab.model_tableau_field }

    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { is_atom_list phil.model_fo_formula_list_field }
    requires { is_atom_list phiacc.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos }
    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        formula_list_disj_semantic clsem m rhos }

    requires { forall m:model int 'st, rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_disj_semantic clsem m rhos <->
        formula_list_disj_semantic phil.model_fo_formula_list_field m rhos \/
        formula_list_disj_semantic phiacc.model_fo_formula_list_field m rhos }
    diverges
    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    let basem = base.model_fo_formula_list_field in
    let tabm = tab.model_tableau_field in
    let tm = t.model_fo_term_list_field in
    let philm = phil.model_fo_formula_list_field in
    let phiaccm = phiacc.model_fo_formula_list_field in
    let phibasem = PApp (Var_symbol p) tm in
    match destruct_fo_formula_list phil with
      | NLC_FOFNil -> raise Failure (* no contradiction found. *)
      | NLC_FOFCons phi0 q -> (* Maybe phi0 is a contradiction. *)
        let phi0m = phi0.model_fo_formula_field in
        let qm = q.model_fo_formula_list_field in
        assert { philm = FOFCons phi0m qm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi0m ->
          is_fo_term_free_var_in_fo_formula_list x philm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x qm ->
          is_fo_term_free_var_in_fo_formula_list x philm && x >= 0 } ;
        assert { is_atom phi0m } ;
        (* prepare backtracking data. *)
        let phiacc2 = construct_fo_formula_list (NLC_FOFCons phi0 phiacc) in
        let phiacc2m = phiacc2.model_fo_formula_list_field in
        assert { phiacc2m = FOFCons phi0m phiaccm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phiacc2m ->
          (is_fo_term_free_var_in_fo_formula x phi0m \/
          is_fo_term_free_var_in_fo_formula_list x phiaccm) && x >= 0 } ;
        match destruct_fo_formula phi0 with
          | NLC_Not phi1 -> let phi1m = phi1.model_fo_formula_field in
            assert { phi0m = Not phi1m } ;
            assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi1m ->
              is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
            match destruct_fo_formula phi1 with
              | NLC_PApp p2 t2 -> match destruct_symbol p2 with
                  | NLCVar_symbol p3 -> let t2m = t2.model_fo_term_list_field in
                    assert { phi1m = PApp (Var_symbol p3) t2m } ;
                    assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t2m ->
                      is_fo_term_free_var_in_fo_formula x phi1m && x >= 0 } ;
                    if p = p3
                    then (* let-try. *)
                      label B in let tp = stamp unifb in
                      let l0 = ref Nil in
                      match try let u = unify_term_list t t2 l0 unifb unif in Some u
                      with UnificationFailure -> None end with
                        (* Contradiction found. *)
                        | Some u -> let unif2 = u.final_unifier in
                          (* should walk back in the tableau
                            until a non-empty branch is found. *)
                          let phifinal = merge phiacc q st in
                          let b = try clause_conflicts phifinal tab unifb unif2;
                            False with Failure -> True end in
                          match b with
                            | True -> label T in backtrack tp unifb ;
                            assert { backtrack_to (unifb at B) (unifb at T) unifb } ;
                          contradiction_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
                            | False -> assert { precede (unifb at B) unifb } ;
                            let phifm = phifinal.model_fo_formula_list_field in
                          assert { forall m:model int 'st,rho:int -> 'st.
                            let rhos = semantic_subst unif2.unifier m rho in
                            let rhos0 = semantic_subst u.unifier_factor m rho in
                            (forall x:int.
                              eval unif2.unifier x = subst_fo_term (eval unif.unifier x)
                                (rcompose identity subst_id_symbol) u.unifier_factor &&
                              rhos x = term_semantic (eval unif2.unifier x) m rho
                                = term_semantic (eval unif.unifier x) (model_rename identity m) rhos0
                                = semantic_subst unif.unifier m rhos0 x) &&
                            extensionalEqual rhos
                              (semantic_subst unif.unifier m rhos0) &&
                            subst_fo_formula phi1m subst_id_symbol unif2.unifier =
                            subst_fo_formula phibasem subst_id_symbol unif2.unifier &&
                            (formula_semantic phi1m m rhos <->
                              formula_semantic phibasem m rhos) &&
                            not(formula_semantic phi0m m rhos /\
                              formula_semantic phibasem m rhos) &&
                            (formula_list_conj_semantic basem m rhos ->
                              tableau_semantic_with tabm True m rhos &&
                              (formula_list_disj_semantic clsem m rhos) &&
                              (formula_list_disj_semantic phifm m rhos \/
                               formula_semantic phi0m m rhos) &&
                              let b = if formula_list_disj_semantic phifm m rhos
                                then True
                                else False in
                              tableau_semantic_with tabm b m rhos) } ;
                          let nd = ref depth in
                          let ct = contract_tableau tab phifinal nd st in
                          let depth = !nd in
                          match ct with
                            | None -> assert { forall m:model int 'st,rho:int -> 'st.
                              let rhos = semantic_subst unif2.unifier m rho in
                              let b = if formula_list_disj_semantic phifm m rhos
                                then True
                                else False in
                              not(tableau_semantic_with tabm b m rhos) &&
                              not(formula_list_conj_semantic basem m rhos) } ;
                              { contradictory_assignment = unif2.unifier }
                            (* continue proof search. If fail,
                             backtrack to find another contradiction. *)
                            | Some tab2 ->
                              let tab2m = tab2.model_tableau_field in
                              assert { forall m:model int 'st,rho:int -> 'st.
                                let rhos = semantic_subst unif2.unifier m rho in
                                formula_list_conj_semantic basem m rhos ->
                                  let b = if formula_list_disj_semantic phifm m rhos
                                    then True
                                    else False in
                                  tableau_semantic_with tabm b m rhos &&
                                  tableau_semantic_with tab2m True m rhos
                                 } ;
                              match !l0 with
                                | Nil -> extend_branch base tab2 unifb unif2 fresh depth goalnum st
                                | _ -> try extend_branch base tab2 unifb unif2 fresh depth goalnum st
                                with Failure ->
                                  label F in backtrack tp unifb ;
                                  assert { backtrack_to (unifb at B) (unifb at F) unifb } ;
                                  try conflict t t2 unifb unif
                                  with UnificationFailure -> raise Failure end ;
                                  contradiction_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
                                end
                              end
                          end end
                        | None -> label N in backtrack tp unifb ;
                          assert { backtrack_to (unifb at B) (unifb at N) unifb } ;
                          contradiction_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
                      end
                    else (* do not conflict. *)
                      contradiction_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
                end
              | _ -> absurd (* phi0 is literal. *)
            end
          | NLC_PApp _ _ -> (* do not conflict. *)
            contradiction_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
          | _ -> absurd (* phi0 is literal. *)
        end
    end

  (* find a contradiction with the current leaf of the tableau,
     if it is a negated literal. *)
  with contradiction_neg_atom (base:nlimpl_fo_formula_list)
      (tab:nlimpl_tableau)
      (unifb:subst)
      (ghost unif:unifier_subst)
      (fresh:int)
      (p:int)
      (t:nlimpl_fo_term_list)
      (ghost phit:fo_formula_list int int)
      (ghost tnext:tableau int int)
      (ghost clsem:fo_formula_list int int)
      (phil:nlimpl_fo_formula_list)
      (phiacc:nlimpl_fo_formula_list)
      (depth:int)
      (goalnum:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok phil }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      phil.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok phiacc }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      phiacc.model_fo_formula_list_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }
    requires { nlimpl_fo_term_list_ok t }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t.model_fo_term_list_field -> x >= 0 }

    requires { tab.model_tableau_field =
      Node tnext (Not (PApp (Var_symbol p) t.model_fo_term_list_field)) phit }

    requires { is_procedure_tableau tab.model_tableau_field }

    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { is_atom_list phil.model_fo_formula_list_field }
    requires { is_atom_list phiacc.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos }
    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        formula_list_disj_semantic clsem m rhos }

    requires { forall m:model int 'st, rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_disj_semantic clsem m rhos <->
        formula_list_disj_semantic phil.model_fo_formula_list_field m rhos \/
        formula_list_disj_semantic phiacc.model_fo_formula_list_field m rhos }
    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    diverges
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    let basem = base.model_fo_formula_list_field in
    let tabm = tab.model_tableau_field in
    let tm = t.model_fo_term_list_field in
    let philm = phil.model_fo_formula_list_field in
    let phiaccm = phiacc.model_fo_formula_list_field in
    let phi1m = PApp (Var_symbol p) tm in
    let phibasem = Not phi1m in
    match destruct_fo_formula_list phil with
      | NLC_FOFNil -> raise Failure (* no contradiction found. *)
      | NLC_FOFCons phi0 q -> (* Maybe phi0 is a contradiction. *)
        let phi0m = phi0.model_fo_formula_field in
        let qm = q.model_fo_formula_list_field in
        assert { philm = FOFCons phi0m qm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi0m ->
          is_fo_term_free_var_in_fo_formula_list x philm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x qm ->
          is_fo_term_free_var_in_fo_formula_list x philm && x >= 0 } ;
        assert { is_atom phi0m } ;
        (* prepare backtracking data. *)
        let phiacc2 = construct_fo_formula_list (NLC_FOFCons phi0 phiacc) in
        let phiacc2m = phiacc2.model_fo_formula_list_field in
        assert { phiacc2m = FOFCons phi0m phiaccm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phiacc2m ->
          (is_fo_term_free_var_in_fo_formula x phi0m \/
          is_fo_term_free_var_in_fo_formula_list x phiaccm) && x >= 0 } ;
        match destruct_fo_formula phi0 with
          | NLC_PApp p2 t2 -> match destruct_symbol p2 with
              | NLCVar_symbol p3 -> let t2m = t2.model_fo_term_list_field in
                assert { phi0m = PApp (Var_symbol p3) t2m } ;
                assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t2m ->
                  is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
                if p = p3
                then (* let-try. *)
                  label B in let tp = stamp unifb in
                  let l0 = ref Nil in
                  match try let u = unify_term_list t t2 l0 unifb unif in Some u
                  with UnificationFailure -> None end with
                    (* Contradiction found. *)
                    | Some u -> let unif2 = u.final_unifier in
                      (* should walk back in the tableau
                        until a non-empty branch is found. *)
                      let phifinal = merge phiacc q st in
                      let b = try clause_conflicts phifinal tab unifb unif2 ;
                        False with Failure -> True end in
                      match b with
                      | True -> label T in backtrack tp unifb ;
                        assert { backtrack_to (unifb at B) (unifb at T) unifb } ;
                        contradiction_neg_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
                      | False -> assert { precede (unifb at B) unifb } ;
                      let phifm = phifinal.model_fo_formula_list_field in
                      assert { forall m:model int 'st,rho:int -> 'st.
                        let rhos = semantic_subst unif2.unifier m rho in
                        let rhos0 = semantic_subst u.unifier_factor m rho in
                        (forall x:int.
                          eval unif2.unifier x = subst_fo_term (eval unif.unifier x)
                            (rcompose identity subst_id_symbol) u.unifier_factor &&
                          rhos x = term_semantic (eval unif2.unifier x) m rho
                            = term_semantic (eval unif.unifier x) (model_rename identity m) rhos0
                            = semantic_subst unif.unifier m rhos0 x) &&
                        extensionalEqual rhos
                         (semantic_subst unif.unifier m rhos0) &&
                        subst_fo_formula phi1m subst_id_symbol unif2.unifier =
                        (*PApp (subst_symbol (Var_symbol p) subst_id_symbol)
                          (subst_fo_term_list tm subst_id_symbol unif2.unifier) =
                        PApp (subst_symbol (Var_symbol p) subst_id_symbol)
                          (subst_fo_term_list t2m subst_id_symbol unif2.unifier) =*)
                        subst_fo_formula phi0m subst_id_symbol unif2.unifier &&
                        (formula_semantic phi0m m rhos <->
                          formula_semantic phi1m m rhos) &&
                        not(formula_semantic phi0m m rhos /\
                          formula_semantic phibasem m rhos) &&
                        (formula_list_conj_semantic basem m rhos ->
                          tableau_semantic_with tabm True m rhos &&
                          (formula_list_disj_semantic clsem m rhos) &&
                          (formula_list_disj_semantic phifm m rhos \/
                           formula_semantic phi0m m rhos) &&
                          let b = if formula_list_disj_semantic phifm m rhos
                            then True
                            else False in
                          tableau_semantic_with tabm b m rhos) } ;
                        let nd = ref depth in
                        let ct = contract_tableau tab phifinal nd st in
                        let depth = !nd in
                      match ct with
                        | None -> assert { forall m:model int 'st,rho:int -> 'st.
                          let rhos = semantic_subst unif2.unifier m rho in
                          let b = if formula_list_disj_semantic phifm m rhos
                            then True
                            else False in
                          not(tableau_semantic_with tabm b m rhos) &&
                          not(formula_list_conj_semantic basem m rhos) } ;
                          { contradictory_assignment = unif2.unifier }
                        (* continue proof search. If fail,
                           backtrack to find another contradiction. *)
                        | Some tab2 ->
                          let tab2m = tab2.model_tableau_field in
                          assert { forall m:model int 'st,rho:int -> 'st.
                            let rhos = semantic_subst unif2.unifier m rho in
                            formula_list_conj_semantic basem m rhos ->
                              let b = if formula_list_disj_semantic phifm m rhos
                                then True
                                else False in
                              tableau_semantic_with tabm b m rhos &&
                              tableau_semantic_with tab2m True m rhos
                            } ;
                          match !l0 with
                            | Nil -> extend_branch base tab2 unifb unif2 fresh depth goalnum st
                            | _ -> try extend_branch base tab2 unifb unif2 fresh depth goalnum st
                              with Failure ->
                                label F in backtrack tp unifb ;
                                assert { backtrack_to (unifb at B) (unifb at F) unifb } ;
                                try conflict t t2 unifb unif
                                with UnificationFailure -> raise Failure end ;
                                contradiction_neg_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
                              end
                          end
                      end end
                    | None -> label N in backtrack tp unifb ;
                      assert { backtrack_to (unifb at B) (unifb at N) unifb } ;
                      contradiction_neg_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
                  end
                else (* do not conflict. *)
                  contradiction_neg_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
            end
          | NLC_Not _ -> (* do not conflict. *)
            contradiction_neg_atom base tab unifb unif fresh p t phit tnext clsem q phiacc2 depth goalnum st
          | _ -> absurd (* phi0 is literal. *)
        end
    end

  (* Technically speaking, the entry point of the main loop.
     Should be called with a preprocessed set of formula
     independent of the interpretation (no free variable),
     and a empty unifier (identity substitution). *)

  with extend_branch (base:nlimpl_fo_formula_list)
      (tab:nlimpl_tableau)
      (unifb:subst)
      (ghost unif:unifier_subst)
      (fresh:int)
      (depth:int)
      (goalnum:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }

    requires { is_procedure_tableau tab.model_tableau_field }
    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos }
    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    diverges
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    let tabm = tab.model_tableau_field in
    let basem = base.model_fo_formula_list_field in
    match destruct_tableau tab with
      | NLC_Root -> if depth = 0
        then raise Failure
        else let depth = depth - 1 in
          select_lemma base base tab unifb unif fresh depth goalnum goalnum st
      | NLC_Node tnext phi0 phib -> let tnextm = tnext.model_tableau_field in
        let phi0m = phi0.model_fo_formula_field in
        let phibm = phib.model_fo_formula_list_field in
        assert { tabm = Node tnextm phi0m phibm } ;
        assert { forall x:int. is_fo_term_free_var_in_tableau x tnextm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi0m ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phibm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { is_atom phi0m } ;
        assert { forall m:model int 'st,rho:int -> 'st.
          let rhos = semantic_subst unif.unifier m rho in
          formula_list_conj_semantic basem m rhos ->
            let b1 = if tableau_node True phibm phi0m m rhos
              then True
              else False in
            tableau_semantic_with tnextm b1 m rhos &&
            (tableau_semantic_with tnextm True m rhos \/
             tableau_semantic_with tnextm False m rhos) } ;
        match destruct_fo_formula phi0 with
          | NLC_PApp ps t -> let psm = ps.model_symbol_field in
            let tm = t.model_fo_term_list_field in
            assert { phi0m = PApp psm tm } ;
            assert { forall x:int. is_fo_term_free_var_in_fo_term_list x tm ->
              is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
            let p = match destruct_symbol ps with
              | NLCVar_symbol p -> assert { psm = Var_symbol p } ; p
            end in
            contradiction_find_atom base tab tnext tnext unifb unif fresh p t phib depth goalnum st
          | NLC_Not phi1 -> let phi1m = phi1.model_fo_formula_field in
            assert { phi0m = Not phi1m } ;
            match destruct_fo_formula phi1 with
              | NLC_PApp ps t ->
                let psm = ps.model_symbol_field in
                let tm = t.model_fo_term_list_field in
                assert { phi1m = PApp psm tm } ;
                assert { forall x:int. is_fo_term_free_var_in_fo_term_list x tm ->
                  is_fo_term_free_var_in_fo_formula x phi1m &&
                  is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
                let p = match destruct_symbol ps with
                  | NLCVar_symbol p -> assert { psm = Var_symbol p } ; p
                end in
                contradiction_find_neg_atom base tab tnext tnext unifb unif fresh p t phib depth goalnum st
              | _ -> absurd
            end
          | _ -> absurd
        end
    end

  (* Look for a contradiction inside the current branch. *)
  with contradiction_find_atom (base:nlimpl_fo_formula_list)
      (tab0 tab1 tab:nlimpl_tableau)
      (unifb:subst)
      (ghost unif:unifier_subst)
      (fresh:int)
      (p:int)
      (t:nlimpl_fo_term_list)
      (philist:nlimpl_fo_formula_list)
      (depth:int)
      (goalnum:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab0 }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab0.model_tableau_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab1 }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab1.model_tableau_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }
    requires { nlimpl_fo_term_list_ok t }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t.model_fo_term_list_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok philist }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      philist.model_fo_formula_list_field -> x >= 0 }

    requires { is_procedure_tableau tab0.model_tableau_field }
    requires { is_procedure_tableau tab.model_tableau_field }

    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { is_atom_list philist.model_fo_formula_list_field }

    requires { tab0.model_tableau_field =
      Node tab1.model_tableau_field
           (PApp (Var_symbol p) t.model_fo_term_list_field)
           philist.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab0.model_tableau_field True m rhos }
    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos \/
        tableau_semantic_with tab.model_tableau_field False m rhos }
    requires { forall m:model int 'st,rho:int -> 'st,b:bool.
      let rhos = semantic_subst unif.unifier m rho in
      (tableau_semantic_with tab.model_tableau_field True m rhos <->
        tableau_semantic_with tab.model_tableau_field False m rhos) ->
      (tableau_semantic_with tab0.model_tableau_field True m rhos <->
       tableau_semantic_with tab0.model_tableau_field False m rhos) }

    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    diverges
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    let tab0m = tab0.model_tableau_field in
    let tab1m = tab1.model_tableau_field in
    let tabm = tab.model_tableau_field in
    let tm = t.model_fo_term_list_field in
    let philm = philist.model_fo_formula_list_field in
    let basem = base.model_fo_formula_list_field in
    let phibasem = PApp (Var_symbol p) tm in
    match destruct_tableau tab with
      | NLC_Root -> (* No branch contradiction found, try to instantiate
        a lemma. *)
        if depth = 0
        then raise Failure
        else select_lemma base base tab0 unifb unif fresh (depth-1) goalnum (-1) st
      | NLC_Node tnext phi0 phib ->
        let tnextm = tnext.model_tableau_field in
        let phi0m = phi0.model_fo_formula_field in
        let phibm = phib.model_fo_formula_list_field in
        assert { tabm = Node tnextm phi0m phibm } ;
        assert { forall x:int. is_fo_term_free_var_in_tableau x tnextm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi0m ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phibm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { is_atom phi0m } ;
        assert { forall m:model int 'st,rho:int -> 'st.
          (tableau_semantic_with tnextm True m rho <->
            tableau_semantic_with tnextm False m rho) ->
          (tableau_semantic_with tabm True m rho <->
            tableau_semantic_with tabm False m rho) } ;
        assert { forall m:model int 'st,rho:int -> 'st,b:bool.
          tableau_semantic_with tabm b m rho ->
            let b1 = if tableau_node b phibm phi0m m rho
              then True
              else False in
            tableau_semantic_with tnextm b1 m rho &&
            (tableau_semantic_with tnextm True m rho \/
             tableau_semantic_with tnextm False m rho) } ;
        match destruct_fo_formula phi0 with
          | NLC_PApp _ _ -> contradiction_find_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
          | NLC_Not phi1 -> let phi1m = phi1.model_fo_formula_field in
            assert { phi0m = Not phi1m } ;
            match destruct_fo_formula phi1 with
              | NLC_PApp p2 t2 ->
                let p2m = p2.model_symbol_field in
                let t2m = t2.model_fo_term_list_field in
                assert { phi1m = PApp p2m t2m } ;
                assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t2m ->
                  is_fo_term_free_var_in_fo_formula x phi1m &&
                  is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
                let p3 = match destruct_symbol p2 with
                    | NLCVar_symbol p3 -> p3
                  end in
                assert { p2m = Var_symbol p3 } ;
                (* Unification attempt. *)
                if p = p3
                then (* let-try. *) label B in let tp = stamp unifb in
                  let l0 = ref Nil in
                  match try let u = unify_term_list t t2 l0 unifb unif in Some u
                  with UnificationFailure -> None end with
                    | Some u -> (* Unifiable. *)
                      let unif2 = u.final_unifier in
                      assert { forall m:model int 'st,rho:int -> 'st.
                        let rhos = semantic_subst unif2.unifier m rho in
                        let rhos0 = semantic_subst u.unifier_factor m rho in
                        (forall x:int.
                          eval unif2.unifier x = subst_fo_term (eval unif.unifier x)
                            (rcompose identity subst_id_symbol) u.unifier_factor &&
                          rhos x = term_semantic (eval unif2.unifier x) m rho
                            = term_semantic (eval unif.unifier x) (model_rename identity m) rhos0
                            = semantic_subst unif.unifier m rhos0 x) &&
                        extensionalEqual rhos
                          (semantic_subst unif.unifier m rhos0) &&
                        subst_fo_formula phi1m subst_id_symbol unif2.unifier =
                        subst_fo_formula phibasem subst_id_symbol unif2.unifier &&
                        (formula_semantic phi1m m rhos <->
                          formula_semantic phibasem m rhos) &&
                        not(formula_semantic phi0m m rhos /\
                          formula_semantic phibasem m rhos) &&
                        (formula_list_conj_semantic basem m rhos ->
                          tableau_semantic_with tab0m True m rhos &&
                          (if formula_semantic phibasem m rhos
                          then (tableau_semantic_with tabm True m rhos <->
                              tableau_semantic_with tabm False m rhos) &&
                            tableau_semantic_with tabm False m rhos &&
                            tableau_semantic_with tab0m False m rhos
                          else tableau_semantic_with tab0m False m rhos) &&
                            tableau_semantic_with tab0m False m rhos &&
                          let b = if formula_list_disj_semantic philm m rhos
                            then True
                            else False in
                          tableau_semantic_with tab1m b m rhos) } ;
                      let nd = ref depth in
                      let ct = contract_tableau tab1 philist nd st in
                      let depth = !nd in
                      match ct with
                        | Some tab2 ->
                          let tab2m = tab2.model_tableau_field in
                          assert { forall m:model int 'st,rho:int -> 'st.
                            let rhos = semantic_subst unif2.unifier m rho in
                            formula_list_conj_semantic basem m rhos ->
                              let b = if formula_list_disj_semantic philm m rhos
                                then True
                                else False in
                              tableau_semantic_with tab1m b m rhos &&
                              tableau_semantic_with tab2m True m rhos
                             } ;
                          match !l0 with
                            | Nil -> extend_branch base tab2 unifb unif2 fresh depth goalnum st
                            | _ -> try extend_branch base tab2 unifb unif2 fresh depth goalnum st
                          with Failure -> label F in
                            backtrack tp unifb ;
                            assert { backtrack_to (unifb at B) (unifb at F) unifb } ;
                            try conflict t t2 unifb unif
                            with UnificationFailure -> raise Failure end ;
                            contradiction_find_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
                          end end
                        | None -> assert { forall m:model int 'st,rho:int -> 'st.
                          let rhos = semantic_subst unif2.unifier m rho in
                          let b = if formula_list_disj_semantic philm m rhos
                            then True
                            else False in
                          not(tableau_semantic_with tab1m b m rhos) &&
                          not(formula_list_conj_semantic basem m rhos) } ;
                          { contradictory_assignment = unif2.unifier }
                      end
                    | None -> label N in backtrack tp unifb ;
                      assert { backtrack_to (unifb at B) (unifb at N) unifb } ;
                      contradiction_find_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
                  end
                else contradiction_find_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
              | _ -> absurd (* atomic. *)
            end
          | _ -> absurd (* atomic. *)
        end
    end

  (* Look for a contradiction inside the current branch,
     negated version. *)
  with contradiction_find_neg_atom (base:nlimpl_fo_formula_list)
      (tab0 tab1 tab:nlimpl_tableau)
      (unifb:subst)
      (ghost unif:unifier_subst)
      (fresh:int)
      (p:int)
      (t:nlimpl_fo_term_list)
      (philist:nlimpl_fo_formula_list)
      (depth:int)
      (goalnum:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab0 }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab0.model_tableau_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab1 }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab1.model_tableau_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }
    requires { nlimpl_fo_term_list_ok t }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t.model_fo_term_list_field -> x >= 0 }
    requires { nlimpl_fo_formula_list_ok philist }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      philist.model_fo_formula_list_field -> x >= 0 }

    requires { is_procedure_tableau tab0.model_tableau_field }
    requires { is_procedure_tableau tab.model_tableau_field }

    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { is_atom_list philist.model_fo_formula_list_field }

    requires { tab0.model_tableau_field =
      Node tab1.model_tableau_field
           (Not (PApp (Var_symbol p) t.model_fo_term_list_field))
           philist.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab0.model_tableau_field True m rhos }
    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos \/
        tableau_semantic_with tab.model_tableau_field False m rhos }
    requires { forall m:model int 'st,rho:int -> 'st,b:bool.
      let rhos = semantic_subst unif.unifier m rho in
      (tableau_semantic_with tab.model_tableau_field True m rhos <->
        tableau_semantic_with tab.model_tableau_field False m rhos) ->
      (tableau_semantic_with tab0.model_tableau_field True m rhos <->
       tableau_semantic_with tab0.model_tableau_field False m rhos) }

    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    diverges
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    let tab0m = tab0.model_tableau_field in
    let tab1m = tab1.model_tableau_field in
    let tabm = tab.model_tableau_field in
    let tm = t.model_fo_term_list_field in
    let philm = philist.model_fo_formula_list_field in
    let basem = base.model_fo_formula_list_field in
    let phi1m = PApp (Var_symbol p) tm in
    let phibasem = Not phi1m in
    match destruct_tableau tab with
      | NLC_Root -> if depth = 0
        then raise Failure
        else select_lemma base base tab0 unifb unif fresh (depth-1) goalnum (-1) st
      | NLC_Node tnext phi0 phib ->
        let tnextm = tnext.model_tableau_field in
        let phi0m = phi0.model_fo_formula_field in
        let phibm = phib.model_fo_formula_list_field in
        assert { tabm = Node tnextm phi0m phibm } ;
        assert { forall x:int. is_fo_term_free_var_in_tableau x tnextm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi0m ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x phibm ->
          is_fo_term_free_var_in_tableau x tabm && x >= 0 } ;
        assert { is_atom phi0m } ;
        assert { forall m:model int 'st,rho:int -> 'st.
          (tableau_semantic_with tnextm True m rho <->
            tableau_semantic_with tnextm False m rho) ->
          (tableau_semantic_with tabm True m rho <->
            tableau_semantic_with tabm False m rho) } ;
        assert { forall m:model int 'st,rho:int -> 'st,b:bool.
          tableau_semantic_with tabm b m rho ->
            let b1 = if tableau_node b phibm phi0m m rho
              then True
              else False in
            tableau_semantic_with tnextm b1 m rho &&
            (tableau_semantic_with tnextm True m rho \/
             tableau_semantic_with tnextm False m rho) } ;
        match destruct_fo_formula phi0 with
          | NLC_Not _ -> contradiction_find_neg_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
          | NLC_PApp p2 t2 ->
            let p2m = p2.model_symbol_field in
            let t2m = t2.model_fo_term_list_field in
            assert { phi0m = PApp p2m t2m } ;
            assert { forall x:int. is_fo_term_free_var_in_fo_term_list x t2m ->
              is_fo_term_free_var_in_fo_formula x phi0m && x >= 0 } ;
            let p3 = match destruct_symbol p2 with
                | NLCVar_symbol p3 -> p3
              end in
            assert { p2m = Var_symbol p3 } ;
            (* Unification attempt. *)
            if p = p3
            then (* let-try. *) label B in let tp = stamp unifb in
              let l0 = ref Nil in
              match try let u = unify_term_list t t2 l0 unifb unif in Some u
              with UnificationFailure -> None end with
                | Some u -> (* Unifiable. *)
                  let unif2 = u.final_unifier in
                  assert { forall m:model int 'st,rho:int -> 'st.
                    let rhos = semantic_subst unif2.unifier m rho in
                    let rhos0 = semantic_subst u.unifier_factor m rho in
                    (forall x:int.
                      eval unif2.unifier x = subst_fo_term (eval unif.unifier x)
                        (rcompose identity subst_id_symbol) u.unifier_factor &&
                      rhos x = term_semantic (eval unif2.unifier x) m rho
                        = term_semantic (eval unif.unifier x) (model_rename identity m) rhos0
                        = semantic_subst unif.unifier m rhos0 x) &&
                    extensionalEqual rhos
                      (semantic_subst unif.unifier m rhos0) &&
                    subst_fo_formula phi1m subst_id_symbol unif2.unifier =
                    subst_fo_formula phi0m subst_id_symbol unif2.unifier &&
                    (formula_semantic phi0m m rhos <->
                      formula_semantic phi1m m rhos) &&
                    not(formula_semantic phi0m m rhos /\
                      formula_semantic phibasem m rhos) &&
                    (formula_list_conj_semantic basem m rhos ->
                      tableau_semantic_with tab0m True m rhos &&
                      (if formula_semantic phibasem m rhos
                      then (tableau_semantic_with tabm True m rhos <->
                          tableau_semantic_with tabm False m rhos) &&
                        tableau_semantic_with tabm False m rhos &&
                        tableau_semantic_with tab0m False m rhos
                      else tableau_semantic_with tab0m False m rhos) &&
                        tableau_semantic_with tab0m False m rhos &&
                      let b = if formula_list_disj_semantic philm m rhos
                        then True
                        else False in
                      tableau_semantic_with tab1m b m rhos) } ;
                  let nd = ref depth in
                  let ct = contract_tableau tab1 philist nd st in
                  let depth = !nd in
                  match ct with
                    | Some tab2 ->
                      let tab2m = tab2.model_tableau_field in
                      assert { forall m:model int 'st,rho:int -> 'st.
                        let rhos = semantic_subst unif2.unifier m rho in
                        formula_list_conj_semantic basem m rhos ->
                        let b = if formula_list_disj_semantic philm m rhos
                          then True
                          else False in
                          tableau_semantic_with tab1m b m rhos &&
                          tableau_semantic_with tab2m True m rhos
                         } ;
                      match !l0 with
                        | Nil -> extend_branch base tab2 unifb unif2 fresh depth goalnum st
                          (* no need to backtrack ! *)
                        | _ -> try
                          extend_branch base tab2 unifb unif2 fresh depth goalnum st
                          with Failure -> label F in
                            backtrack tp unifb ;
                            assert { backtrack_to (unifb at B) (unifb at F) unifb } ;
                            try conflict t t2 unifb unif
                            with UnificationFailure -> raise Failure end;
                            contradiction_find_neg_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
                          end end
                    | None -> assert { forall m:model int 'st,rho:int -> 'st.
                      let rhos = semantic_subst unif2.unifier m rho in
                      let b = if formula_list_disj_semantic philm m rhos
                        then True
                        else False in
                      not(tableau_semantic_with tab1m b m rhos) &&
                      not(formula_list_conj_semantic basem m rhos) } ;
                      { contradictory_assignment = unif2.unifier }
                  end
                | None -> label N in backtrack tp unifb ;
                  assert { backtrack_to (unifb at B) (unifb at N) unifb } ;
                  contradiction_find_neg_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
              end
            else contradiction_find_neg_atom base tab0 tab1 tnext unifb unif fresh p t philist depth goalnum st
          | _ -> absurd (* atomic. *)
        end
    end

  (* Iterate through every lemma of the base formula set. *)

  with select_lemma (base:nlimpl_fo_formula_list) (basecursor:nlimpl_fo_formula_list)
    (tab:nlimpl_tableau)
    (unifb:subst)
    (ghost unif:unifier_subst)
    (fresh:int)
    (depth:int)
    (goalnum:int)
    (number:int) (ghost st:'st) : prover_return
    requires { fresh >= 0 }
    requires { nlimpl_fo_formula_list_ok base }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      base.model_fo_formula_list_field -> x >= 0 }
    requires { nlimpl_tableau_ok tab }
    requires { forall x:int. is_fo_term_free_var_in_tableau x
      tab.model_tableau_field -> x >= 0 }
    requires { unifier_subst_ok unifb unif }
    requires { nlimpl_fo_formula_list_ok basecursor }
    requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x
      basecursor.model_fo_formula_list_field -> x >= 0 }

    requires { is_procedure_tableau tab.model_tableau_field }

    requires { is_simpl_list base.model_fo_formula_list_field }
    requires { is_nnf_list base.model_fo_formula_list_field }
    requires { no_existential_list base.model_fo_formula_list_field }

    requires { is_simpl_list basecursor.model_fo_formula_list_field }
    requires { is_nnf_list basecursor.model_fo_formula_list_field }
    requires { no_existential_list basecursor.model_fo_formula_list_field }

    requires { forall m:model int 'st,rho:int -> 'st.
      formula_list_conj_semantic base.model_fo_formula_list_field m rho ->
        formula_list_conj_semantic basecursor.model_fo_formula_list_field m rho }

    requires { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst unif.unifier m rho in
      formula_list_conj_semantic base.model_fo_formula_list_field m rhos ->
        tableau_semantic_with tab.model_tableau_field True m rhos }

    ensures { forall m:model int 'st,rho:int -> 'st.
      let rhos = semantic_subst result.contradictory_assignment m rho in
      not(formula_list_conj_semantic base.model_fo_formula_list_field m rhos) }
    ensures { precede (old unifb) unifb /\ correct unifb }
    diverges
    raises { Failure -> precede (old unifb) unifb /\ correct unifb }
  =
    if number = 0
    then raise Failure ;
    let bcm = basecursor.model_fo_formula_list_field in
    match destruct_fo_formula_list basecursor with
      | NLC_FOFNil -> raise Failure
      | NLC_FOFCons x q -> let qm = q.model_fo_formula_list_field in
        let xm = x.model_fo_formula_field in
        assert { bcm = FOFCons xm qm } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula x xm ->
          is_fo_term_free_var_in_fo_formula_list x bcm && x >= 0 } ;
        assert { forall x:int. is_fo_term_free_var_in_fo_formula_list x qm ->
          is_fo_term_free_var_in_fo_formula_list x bcm && x >= 0 } ;
        let fonil = construct_fo_formula_list NLC_FOFNil in
        assert { fonil.model_fo_formula_list_field = FOFNil } ;
        label B in let tp = stamp unifb in
        try decompose base tab unifb unif fresh x fonil fonil depth goalnum st
        with Failure -> label F in backtrack tp unifb ;
          assert { backtrack_to (unifb at B) (unifb at F) unifb } ;
          select_lemma base q tab unifb unif fresh depth goalnum (number-1) st end
    end

end