Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Proof by Reflection

Authors: Adam Chlipala
summary:A chapter from CPDT (CC-BY), used to demo Alectryon

The last chapter highlighted a very heuristic approach to proving. As an alternative, we will study a technique called proof by reflection. We will write, in Gallina (the logical functional-programming language of Coq), decision procedures with proofs of correctness, and we will appeal to these procedures in writing very short proofs. Such a proof is checked by running the decision procedure. The term reflection applies because we will need to translate Gallina propositions into values of inductive types representing syntax, so that Gallina programs may analyze them, and translating such a term back to the original form is called reflecting it.

Proving Evenness

Proving that particular natural number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned last week make it easy to implement such a procedure.

Inductive isEven : nat -> Prop :=
| Even_O : isEven O
| Even_SS : forall n, isEven n -> isEven (S (S n)).

Ltac prove_even := repeat constructor.


isEven 256
prove_even. Qed.
even_256 = @Even_SS (S (S (S (S (S (S (S (S (S (S (S (S (...))))))))))))) (@Even_SS (S (S (S (S (S (S (S (S (S (S (S (...)))))))))))) (@Even_SS (S (S (S (S (S (S (S (S (S (S (...))))))))))) (@Even_SS (S (S (S (S (S (S (S (S (S (...)))))))))) (@Even_SS (S (S (S (S (S (S (S (S (...))))))))) (@Even_SS (S (S (S (S (S (S (S (...)))))))) (@Even_SS (S (S (S (S (S (S (...))))))) (@Even_SS (S (S (S (S (S (...)))))) (@Even_SS (S (S (S (S (...))))) (@Even_SS (S (S (S (...)))) (@Even_SS (S (S (...))) (@Even_SS (S (...)) (@Even_SS (...) (...))))))))))))) : isEven (S (S (S (S (S (S (S (S (S (S (S (S (...)))))))))))))

Here we see a term of Coq's core proof language, which we don't explain in detail, but roughly speaking such a term is a syntax tree recording which lemmas were used, and how their quantifiers were instantiated, to prove a theorem. This Ltac procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even. The final proof term has length super-linear in the input value, which we reveal with Set Printing All, to disable all syntactic niceties and show every node of the internal proof AST. The problem is that each Even_SS application needs a choice of n, and we wind up giving every even number from 0 to 254 in that position, at some point or another, for quadratic proof-term size.

It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately. Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals.

The techniques of proof by reflection address both complaints. We will be able to write proofs like in the example above with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.

Fixpoint check_even (n : nat) : bool :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n') => check_even n'
  end.

To prove check_even sound, we need two IH strengthenings:

  • Effectively switch to strong induction with an extra numeric variable, asserted to be less than the one we induct on.
  • Express both cases for how a check_even test might turn out.

forall n n' : nat, n' < n -> if check_even n' then isEven n' else ~ isEven n'
n':nat
H:n' < 0

if check_even n' then isEven n' else ~ isEven n'
n:nat
IHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0
n':nat
H:n' < S n
if check_even n' then isEven n' else ~ isEven n'
n:nat
IHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0
n':nat
H:n' < S n

if check_even n' then isEven n' else ~ isEven n'
n:nat
IHn:forall n' : nat, n' < n -> if check_even n' then isEven n' else ~ isEven n'
H:0 < S n

isEven 0
n:nat
IHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0
n':nat
H:S n' < S n
if match n' with | 0 => false | S n'0 => check_even n'0 end then isEven (S n') else ~ isEven (S n')
n:nat
IHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0
n':nat
H:S n' < S n

if match n' with | 0 => false | S n'0 => check_even n'0 end then isEven (S n') else ~ isEven (S n')
n:nat
IHn:forall n' : nat, n' < n -> if check_even n' then isEven n' else ~ isEven n'
H:1 < S n

~ isEven 1
n:nat
IHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0
n':nat
H:S (S n') < S n
if check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))
n:nat
IHn:forall n' : nat, n' < n -> if check_even n' then isEven n' else isEven n' -> False
H:1 < S n
H0:isEven 1

False
n:nat
IHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0
n':nat
H:S (S n') < S n
if check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))
n:nat
IHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0
n':nat
H:S (S n') < S n

if check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))
n, n':nat
IHn:n' < n -> if check_even n' then isEven n' else ~ isEven n'
H:S (S n') < S n

if check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))
n, n':nat
Heq:check_even n' = true
IHn:n' < n -> isEven n'
H:S (S n') < S n

isEven (S (S n'))
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> ~ isEven n'
H:S (S n') < S n
~ isEven (S (S n'))
n, n':nat
Heq:check_even n' = true
IHn:n' < n -> isEven n'
H:S (S n') < S n

isEven n'
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> ~ isEven n'
H:S (S n') < S n
~ isEven (S (S n'))
n, n':nat
Heq:check_even n' = true
IHn:n' < n -> isEven n'
H:S (S n') < S n

n' < n
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> ~ isEven n'
H:S (S n') < S n
~ isEven (S (S n'))
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> ~ isEven n'
H:S (S n') < S n

~ isEven (S (S n'))
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> isEven n' -> False
H:S (S n') < S n
H0:isEven (S (S n'))

False
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> isEven n' -> False
H:S (S n') < S n
H2:isEven n'

False
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> isEven n' -> False
H:S (S n') < S n
H2:isEven n'

n' < n
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> isEven n' -> False
H:S (S n') < S n
H2:isEven n'
isEven n'
n, n':nat
Heq:check_even n' = false
IHn:n' < n -> isEven n' -> False
H:S (S n') < S n
H2:isEven n'

isEven n'
assumption. Qed.

forall n : nat, check_even n = true -> isEven n
n:nat
H:check_even n = true

isEven n
n:nat
H:check_even n = true
H0:n < S n

isEven n
n:nat
H:check_even n = true
H0:if check_even n then isEven n else ~ isEven n

isEven n
n:nat
H:check_even n = true
H0:isEven n

isEven n
assumption. Qed.

As this theorem establishes, the function check_even may be viewed as a verified decision procedure. It is now trivial to write a tactic to prove evenness.

Ltac prove_even_reflective :=
  match goal with
    | [ |- isEven ?N] => apply check_even_ok; reflexivity
  end.


isEven 256
prove_even_reflective. Qed.
even_256' = check_even_ok (S (S (S (S (S (S (S (S (S (S (S (S (...))))))))))))) (@eq_refl bool true) : isEven (S (S (S (S (S (S (S (S (S (S (S (S (...)))))))))))))

Notice that only one nat appears as an argument to an applied lemma, and that's the original number to test for evenness. Proof-term size scales linearly.

What happens if we try the tactic with an odd number?


isEven 255
Unable to unify "true" with "check_even 255".

isEven 255
Abort.

Coq reports that reflexivity can't prove false = true, which makes perfect sense!

Our tactic prove_even_reflective is reflective because it performs a proof-search process (a trivial one, in this case) wholly within Gallina.

Reifying the Syntax of a Trivial Tautology Language

We might also like to have reflective proofs of trivial tautologies like this one:


True /\ True -> True \/ True /\ (True -> True)
tauto. Qed.
true_galore = fun H : True /\ True => and_ind (fun _ _ : True => or_introl I) H : True /\ True -> True \/ True /\ (True -> True)

As we might expect, the proof that tauto builds contains explicit applications of deduction rules. For large formulas, this can add a linear amount of proof-size overhead, beyond the size of the input.

To write a reflective procedure for this class of goals, we will need to get into the actual "reflection" part of "proof by reflection." It is impossible to case-analyze a Prop in any way in Gallina. We must reify Prop into some type that we can analyze. This inductive type is a good candidate:

Inductive taut : Set :=
| TautTrue : taut
| TautAnd : taut -> taut -> taut
| TautOr : taut -> taut -> taut
| TautImp : taut -> taut -> taut.

We write a recursive function to reflect this syntax back to Prop. Such functions are also called interpretation functions, and we have used them in previous examples to give semantics to small programming languages.

Fixpoint tautDenote (t : taut) : Prop :=
  match t with
    | TautTrue => True
    | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
    | TautOr t1 t2 => tautDenote t1 \/ tautDenote t2
    | TautImp t1 t2 => tautDenote t1 -> tautDenote t2
  end.

It is easy to prove that every formula in the range of tautDenote is true.


forall t : taut, tautDenote t
induct t; simplify; propositional. Qed.

To use tautTrue to prove particular formulas, we need to implement the syntax-reification process. A recursive Ltac function does the job.

Ltac tautReify P :=
  match P with
    | True => TautTrue
    | ?P1 /\ ?P2 =>
      let t1 := tautReify P1 in
      let t2 := tautReify P2 in
        constr:(TautAnd t1 t2)
    | ?P1 \/ ?P2 =>
      let t1 := tautReify P1 in
      let t2 := tautReify P2 in
        constr:(TautOr t1 t2)
    | ?P1 -> ?P2 =>
      let t1 := tautReify P1 in
      let t2 := tautReify P2 in
        constr:(TautImp t1 t2)
  end.

With tautReify available, it is easy to finish our reflective tactic. We look at the goal formula, reify it, and apply tautTrue to the reified formula. Recall that the change tactic replaces a conclusion formula with another that is equal to it, as shown by partial execution of terms.

Ltac obvious :=
  match goal with
    | [ |- ?P ] =>
      let t := tautReify P in
      change (tautDenote t); apply tautTrue
  end.

We can verify that obvious solves our original example, with a proof term that does not mention details of the proof.


True /\ True -> True \/ True /\ (True -> True)
obvious. Qed.
true_galore' = tautTrue (TautImp (TautAnd TautTrue TautTrue) (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue)))) : forall _ : and True True, or True (and True (forall _ : True, True))

It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula-reification process is just as ad-hoc as before, so we gain little there. In general, proofs will be more complicated than formula translation, and the "generic proof rule" that we apply here is on much better formal footing than a recursive Ltac function. The dependent type of the proof guarantees that it "works" on any input formula. This benefit is in addition to the proof-size improvement that we have already seen.

It may also be worth pointing out that our previous example of evenness testing used a test check_even that could sometimes fail, while here we avoid the extra Boolean test by identifying a syntactic class of formulas that are always true by construction. Of course, many interesting proof steps don't have that structure, so let's look at an example that still requires extra proving after the reflective step.

A Monoid Expression Simplifier

Proof by reflection does not require encoding of all of the syntax in a goal. We can insert "variables" in our syntax types to allow injection of arbitrary pieces, even if we cannot apply specialized reasoning to them. In this section, we explore that possibility by writing a tactic for normalizing monoid equations.

Section monoid.
  Variable A : Set.
  Variable e : A.
  Variable f : A -> A -> A.

  Infix "+" := f.

  Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c).
  Hypothesis identl : forall a, e + a = a.
  Hypothesis identr : forall a, a + e = a.

We add variables and hypotheses characterizing an arbitrary instance of the algebraic structure of monoids. We have an associative binary operator and an identity element for it.

It is easy to define an expression-tree type for monoid expressions. A Var constructor is a "catch-all" case for subexpressions that we cannot model. These subexpressions could be actual Gallina variables, or they could just use functions that our tactic is unable to understand.

  Inductive mexp : Set :=
  | Ident : mexp
  | Var : A -> mexp
  | Op : mexp -> mexp -> mexp.

Next, we write an interpretation function.

  Fixpoint mdenote (me : mexp) : A :=
    match me with
      | Ident => e
      | Var v => v
      | Op me1 me2 => mdenote me1 + mdenote me2
    end.

We will normalize expressions by flattening them into lists, via associativity, so it is helpful to have a denotation function for lists of monoid values.

  Fixpoint mldenote (ls : list A) : A :=
    match ls with
      | nil => e
      | x :: ls' => x + mldenote ls'
    end.

The flattening function itself is easy to implement.

  Fixpoint flatten (me : mexp) : list A :=
    match me with
      | Ident => []
      | Var x => [x]
      | Op me1 me2 => flatten me1 ++ flatten me2
    end.

This function has a straightforward correctness proof in terms of our denote functions.

  
A:Set
e:A
f:A -> A -> A
assoc:forall a b c : A, a + b + c = a + (b + c)
identl:forall a : A, e + a = a
identr:forall a : A, a + e = a

forall ml2 ml1 : list A, mldenote (ml1 ++ ml2) = mldenote ml1 + mldenote ml2
induction ml1; simplify; equality. Qed. Hint Rewrite flatten_correct'.
A:Set
e:A
f:A -> A -> A
assoc:forall a b c : A, a + b + c = a + (b + c)
identl:forall a : A, e + a = a
identr:forall a : A, a + e = a

forall me : mexp, mdenote me = mldenote (flatten me)
induction me; simplify; equality. Qed.

Now it is easy to prove a theorem that will be the main tool behind our simplification tactic.

  
A:Set
e:A
f:A -> A -> A
assoc:forall a b c : A, a + b + c = a + (b + c)
identl:forall a : A, e + a = a
identr:forall a : A, a + e = a

forall me1 me2 : mexp, mldenote (flatten me1) = mldenote (flatten me2) -> mdenote me1 = mdenote me2
simplify; repeat rewrite flatten_correct; assumption. Qed.

We implement reification into the mexp type.

  Ltac reify me :=
    match me with
      | e => Ident
      | ?me1 + ?me2 =>
        let r1 := reify me1 in
        let r2 := reify me2 in
          constr:(Op r1 r2)
      | _ => constr:(Var me)
    end.

The final monoid tactic works on goals that equate two monoid terms. We reify each and change the goal to refer to the reified versions, finishing off by applying monoid_reflect and simplifying uses of mldenote.

  Ltac monoid :=
    match goal with
      | [ |- ?me1 = ?me2 ] =>
        let r1 := reify me1 in
        let r2 := reify me2 in
          change (mdenote r1 = mdenote r2);
            apply monoid_reflect; simplify
    end.

We can make short work of theorems like this one:

  
A:Set
e:A
f:A -> A -> A
assoc:forall a b c : A, a + b + c = a + (b + c)
identl:forall a : A, e + a = a
identr:forall a : A, a + e = a

forall a b c d : A, a + b + c + d = a + (b + c) + d
A:Set
e:A
f:A -> A -> A
assoc:forall a0 b0 c0 : A, a0 + b0 + c0 = a0 + (b0 + c0)
identl:forall a0 : A, e + a0 = a0
identr:forall a0 : A, a0 + e = a0
a, b, c, d:A

a + (b + (c + (d + e))) = a + (b + (c + (d + e)))

Our tactic has canonicalized both sides of the equality, such that we can finish the proof by reflexivity.

    reflexivity.
  Qed.

It is interesting to look at the form of the proof.

    
t1 = (fun a b c d : A => monoid_reflect (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d)) (Op (Op (Var a) (Op (Var b) (Var c))) (Var d)) (@eq_refl A (f a (f b (f c (f d e)))) : @eq A (mldenote (flatten (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d)))) (mldenote (flatten (Op (Op (Var a) (Op (Var b) (Var c))) (Var d)))))) : forall a b c d : A, @eq A (f (f (f a b) c) d) (f (f a (f b c)) d) : forall a b c d : A, @eq A (f (f (f a b) c) d) (f (f a (f b c)) d)

The proof term contains only restatements of the equality operands in reified form, followed by a use of reflexivity on the shared canonical form.

End monoid.

Extensions of this basic approach are used in the implementations of the ring and field tactics that come packaged with Coq.

Set Simplification for Model Checking

Let's take a closer look at model-checking proofs like from last class.

Here's a simple transition system, where state is just a nat, and where each step subtracts 1 or 2.

Inductive subtract_step : nat -> nat -> Prop :=
| Subtract1 : forall n, subtract_step (S n) n
| Subtract2 : forall n, subtract_step (S (S n)) n.

Definition subtract_sys (n : nat) : trsys nat := {|
  Initial := {n};
  Step := subtract_step
|}.


invariantFor (subtract_sys 5) (fun n : nat => n <= 5)

invariantFor (subtract_sys 5) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) (Initial (subtract_sys 5)) (Initial (subtract_sys 5)) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5} {5} ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

Here we'll see that the Frap libary uses slightly different, optimized versions of the model-checking relations. For instance, multiStepClosure takes an extra set argument, the worklist recording newly discovered states. There is no point in following edges out of states that were already known at previous steps.

Now, some more manual iterations:

  

oneStepClosure (subtract_sys 5) {5} ?inv'

multiStepClosure (subtract_sys 5) ({5} \cup ?inv') (?inv' \setminus {5}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5
4
3
3

multiStepClosure (subtract_sys 5) ({5} \cup (({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { })) ((({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { }) \setminus {5}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

Ew. What a big, ugly set expression. Let's shrink it down to something more readable, with duplicates removed, etc.

  

multiStepClosure (subtract_sys 5) {5, 4, 3} {4, 3} ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

How does the Frap library do that? Proof by reflection is a big part of it! Let's develop a baby version of that automation. The full-scale version is in file Sets.v.

Abort.

We'll specialize our representation to unions of set literals, whose elements are constant nats. The full-scale version in the library is more flexible.

Inductive setexpr :=
| Literal (ns : list nat)
| Union (e1 e2 : setexpr).

Here's what our expressions mean.

Fixpoint setexprDenote (e : setexpr) : set nat :=
  match e with
  | Literal ns => constant ns
  | Union e1 e2 => setexprDenote e1 \cup setexprDenote e2
  end.

Simplification reduces all expressions to flat, duplicate-free set literals.

Fixpoint normalize (e : setexpr) : list nat :=
  match e with
  | Literal ns => dedup ns
  | Union e1 e2 => setmerge (normalize e1) (normalize e2)
  end.

Here we use functions dedup and setmerge from the Sets module, which is especially handy because that module has proved some key theorems about them.

Let's prove that normalization doesn't change meaning.


forall e : setexpr, setexprDenote e = constant (normalize e)

Here we use the more primitive simpl, because simplify calls the fancier set automation from the book library, which would be "cheating."

  
ns:list nat

constant ns = constant (dedup ns)
e1, e2:setexpr
IHe1:setexprDenote e1 = constant (normalize e1)
IHe2:setexprDenote e2 = constant (normalize e2)
setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))
ns:list nat
H:constant (map (fun x : nat => x) (dedup ns)) = constant (map (fun x : nat => x) ns)

constant ns = constant (dedup ns)
e1, e2:setexpr
IHe1:setexprDenote e1 = constant (normalize e1)
IHe2:setexprDenote e2 = constant (normalize e2)
setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))
ns:list nat
H:constant (dedup ns) = constant ns

constant ns = constant (dedup ns)
e1, e2:setexpr
IHe1:setexprDenote e1 = constant (normalize e1)
IHe2:setexprDenote e2 = constant (normalize e2)
setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))
e1, e2:setexpr
IHe1:setexprDenote e1 = constant (normalize e1)
IHe2:setexprDenote e2 = constant (normalize e2)

setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))
e1, e2:setexpr
IHe1:setexprDenote e1 = constant (normalize e1)
IHe2:setexprDenote e2 = constant (normalize e2)

constant (normalize e1) \cup constant (normalize e2) = constant (setmerge (normalize e1) (normalize e2))
e1, e2:setexpr
IHe1:setexprDenote e1 = constant (normalize e1)
IHe2:setexprDenote e2 = constant (normalize e2)
H:constant (map (fun x : nat => x) (setmerge (normalize e1) (normalize e2))) = constant (map (fun x : nat => x) (normalize e1)) \cup constant (map (fun x : nat => x) (normalize e2))

constant (normalize e1) \cup constant (normalize e2) = constant (setmerge (normalize e1) (normalize e2))
e1, e2:setexpr
IHe1:setexprDenote e1 = constant (normalize e1)
IHe2:setexprDenote e2 = constant (normalize e2)
H:constant (setmerge (normalize e1) (normalize e2)) = constant (normalize e1) \cup constant (normalize e2)

constant (normalize e1) \cup constant (normalize e2) = constant (setmerge (normalize e1) (normalize e2))
equality. Qed.

Reification works as before, with one twist.

Ltac reify_set E :=
  match E with
  | constant ?ns => constr:(Literal ns)
  | ?E1 \cup ?E2 =>
    let e1 := reify_set E1 in
    let e2 := reify_set E2 in
    constr:(Union e1 e2)
  | _ => let pf := constr:(E = {}) in constr:(Literal [])
  end.

The twist is in this last case: we instantiate all unification variables with the empty set. It's a sound proof step, and it so happens that we only call this tactic in spots where this heuristic makes sense.

Now the usual recipe for a reflective tactic, this time using rewriting instead of apply for the key step, to allow simplification deep within the structure of a goal.

Ltac simplify_set :=
  match goal with
  | [ |- context[?X \cup ?Y] ] =>
    let e := reify_set (X \cup Y) in
    let Heq := fresh in
    assert (Heq : X \cup Y = setexprDenote e) by reflexivity;
    rewrite Heq; clear Heq;
    rewrite normalize_ok; simpl
  end.

Back to our example, which we can now finish without calling simplify to reduces trees of union operations.


invariantFor (subtract_sys 5) (fun n : nat => n <= 5)

invariantFor (subtract_sys 5) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) (Initial (subtract_sys 5)) (Initial (subtract_sys 5)) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5} {5} ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

Now, some more manual iterations:

  

oneStepClosure (subtract_sys 5) {5} ?inv'

multiStepClosure (subtract_sys 5) ({5} \cup ?inv') (?inv' \setminus {5}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5
4
3
3

multiStepClosure (subtract_sys 5) ({5} \cup (({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { })) ((({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { }) \setminus {5}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3} ((({5} \cup ({4} \cup ({3} \cup { }))) \cup { }) \setminus {5}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

Success! One subexpression shrunk. Now for the other.

  

multiStepClosure (subtract_sys 5) {5, 4, 3} ({5, 4, 3} \setminus {5}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

Our automation doesn't handle set difference, so we finish up calling the library tactic.

  

multiStepClosure (subtract_sys 5) {5, 4, 3} {4, 3} ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

oneStepClosure (subtract_sys 5) {4, 3} ?inv'

multiStepClosure (subtract_sys 5) ({5, 4, 3} \cup ?inv') (?inv' \setminus {5, 4, 3}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5
3
2
2
2
1
1

multiStepClosure (subtract_sys 5) ({5, 4, 3} \cup (({4} \cup ({3} \cup ({2} \cup ?rest))) \cup (({3} \cup ({2} \cup ({1} \cup ?rest0))) \cup { }))) ((({4} \cup ({3} \cup ({2} \cup ?rest))) \cup (({3} \cup ({2} \cup ({1} \cup ?rest0))) \cup { })) \setminus {5, 4, 3}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1} ((({4} \cup ({3} \cup ({2} \cup { }))) \cup (({3} \cup ({2} \cup ({1} \cup { }))) \cup { })) \setminus {5, 4, 3}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1} ({4, 3, 2, 1} \setminus {5, 4, 3}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1} {2, 1} ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

oneStepClosure (subtract_sys 5) {2, 1} ?inv'

multiStepClosure (subtract_sys 5) ({5, 4, 3, 2, 1} \cup ?inv') (?inv' \setminus {5, 4, 3, 2, 1}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5
1
0
0
0

multiStepClosure (subtract_sys 5) ({5, 4, 3, 2, 1} \cup (({2} \cup ({1} \cup ({0} \cup ?rest))) \cup (({1} \cup ({0} \cup ?rest0)) \cup { }))) ((({2} \cup ({1} \cup ({0} \cup ?rest))) \cup (({1} \cup ({0} \cup ?rest0)) \cup { })) \setminus {5, 4, 3, 2, 1}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} ((({2} \cup ({1} \cup ({0} \cup { }))) \cup (({1} \cup ({0} \cup { })) \cup { })) \setminus {5, 4, 3, 2, 1}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} ({2, 1, 0} \setminus {5, 4, 3, 2, 1}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} {0} ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

oneStepClosure (subtract_sys 5) {0} ?inv'

multiStepClosure (subtract_sys 5) ({5, 4, 3, 2, 1, 0} \cup ?inv') (?inv' \setminus {5, 4, 3, 2, 1, 0}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) ({5, 4, 3, 2, 1, 0} \cup (({0} \cup ?inv1) \cup { })) ((({0} \cup ?inv1) \cup { }) \setminus {5, 4, 3, 2, 1, 0}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} ((({0} \cup { }) \cup { }) \setminus {5, 4, 3, 2, 1, 0}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} ({0} \setminus {5, 4, 3, 2, 1, 0}) ?invariant1

forall s : nat, ?invariant1 s -> s <= 5

multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} { } ?invariant1

forall s : nat, ?invariant1 s -> s <= 5
4
3
3
3
2
2
2
1
1
1
0
0
0

forall s : nat, {5, 4, 3, 2, 1, 0} s -> s <= 5
s:nat
H:5 = s \/ 4 = s \/ 3 = s \/ 2 = s \/ 1 = s \/ 0 = s \/ False

s <= 5
linear_arithmetic. Qed.

A Smarter Tautology Solver

Now we are ready to revisit our earlier tautology-solver example. We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent. We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example. Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas. For instance, we cannot prove P -> P by translating the formula into a value like Imp (Var P) (Var P), because a Gallina function has no way of comparing the two Ps for equality.

We introduce a synonym for how we name variables: natural numbers.

Definition propvar := nat.

Inductive formula : Set :=
| Atomic : propvar -> formula
| Truth : formula
| Falsehood : formula
| And : formula -> formula -> formula
| Or : formula -> formula -> formula
| Imp : formula -> formula -> formula.

Now we can define our denotation function. First, a type of truth-value assignments to propositional variables:

Definition asgn := nat -> Prop.

Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
  match f with
    | Atomic v => atomics v
    | Truth => True
    | Falsehood => False
    | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
    | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
    | Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2
  end.

Section my_tauto.
  Variable atomics : asgn.

Now we are ready to define some helpful functions based on the ListSet module of the standard library, which (unsurprisingly) presents a view of lists as sets.

  
Use of “Requireinside a section is deprecated. [require-in-section,deprecated]

The eq_nat_dec below is a richly typed equality test on nats. We'll get to the ideas behind it in a later class.

  Definition add (s : set propvar) (v : propvar) :=
    set_add eq_nat_dec v s.

We define what it means for all members of a variable set to represent true propositions, and we prove some lemmas about this notion.

  Fixpoint allTrue (s : set propvar) : Prop :=
    match s with
      | nil => True
      | v :: s' => atomics v /\ allTrue s'
    end.

  
atomics:asgn

forall (v : nat) (s : set propvar), allTrue s -> atomics v -> allTrue (add s v)
induct s; simplify; propositional; match goal with | [ |- context[if ?E then _ else _] ] => destruct E end; simplify; propositional. Qed.
atomics:asgn

forall (v : propvar) (s : set propvar), allTrue s -> set_In v s -> atomics v
induct s; simplify; equality. Qed.

Now we can write a function forward that implements deconstruction of hypotheses, expanding a compound formula into a set of sets of atomic formulas covering all possible cases introduced with use of Or. To handle consideration of multiple cases, the function takes in a continuation argument (advanced functional-programming feature that often puzzles novices, so don't worry if it takes a while to digest!), which will be called once for each case.

  Fixpoint forward (f : formula) (known : set propvar) (hyp : formula)
           (cont : set propvar -> bool) : bool :=
    match hyp with
    | Atomic v => cont (add known v)
    | Truth => cont known
    | Falsehood => true
    | And h1 h2 => forward (Imp h2 f) known h1 (fun known' =>
                     forward f known' h2 cont)
    | Or h1 h2 => forward f known h1 cont && forward f known h2 cont
    | Imp _ _ => cont known
    end.

A backward function implements analysis of the final goal. It calls forward to handle implications.

  Fixpoint backward (known : set propvar) (f : formula) : bool :=
    match f with
    | Atomic v => if In_dec eq_nat_dec v known then true else false
    | Truth => true
    | Falsehood => false
    | And f1 f2 => backward known f1 && backward known f2
    | Or f1 f2 => backward known f1 || backward known f2
    | Imp f1 f2 => forward f2 known f1
                     (fun known' => backward known' f2)
    end.
End my_tauto.


forall (atomics : asgn) (hyp f : formula) (known : set propvar) (cont : set propvar -> bool), forward f known hyp cont = true -> (forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f) -> allTrue atomics known -> formulaDenote atomics hyp -> formulaDenote atomics f
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p

formulaDenote atomics f
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p

allTrue atomics (add known p)
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p
cont (add known p) = true
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p

allTrue atomics known
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p
atomics p
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p
cont (add known p) = true
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p

atomics p
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p
cont (add known p) = true
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
p:propvar
f:formula
known:set propvar
cont:set propvar -> bool
H:cont (add known p) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:atomics p

cont (add known p) = true
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True

allTrue atomics ?known'
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True
cont ?known' = true
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:True

cont known = true
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:formulaDenote atomics (Imp hyp2 f)
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
forall known' : set propvar, allTrue atomics known' -> forward f known' hyp2 cont = true -> formulaDenote atomics (Imp hyp2 f)
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2

forall known' : set propvar, allTrue atomics known' -> forward f known' hyp2 cont = true -> formulaDenote atomics (Imp hyp2 f)
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2

forward f ?known hyp2 ?cont = true
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2
forall known'0 : set propvar, allTrue atomics known'0 -> ?cont known'0 = true -> formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2
allTrue atomics ?known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2
formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2

forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2
allTrue atomics known'
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2
formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2

allTrue atomics known'
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2
formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known'0 : set propvar, allTrue atomics known'0 -> cont0 known'0 = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = true
H0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
known':set propvar
H2:allTrue atomics known'
H5:forward f known' hyp2 cont = true
H6:formulaDenote atomics hyp2

formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2

allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H4:formulaDenote atomics hyp2

formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

forward f ?known hyp1 ?cont = true
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
forall known' : set propvar, allTrue atomics known' -> ?cont known' = true -> formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
allTrue atomics ?known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp1
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

formulaDenote atomics hyp1
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:forward f known hyp1 cont && forward f known hyp2 cont = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

forward f ?known hyp2 ?cont = true
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
forall known' : set propvar, allTrue atomics known' -> ?cont known' = true -> formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
allTrue atomics ?known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

allTrue atomics known
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true
formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H3:formulaDenote atomics hyp2
H2:forward f known hyp1 cont = true
H4:forward f known hyp2 cont = true

formulaDenote atomics hyp2
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2

formulaDenote atomics f
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2

allTrue atomics ?known'
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2
cont ?known' = true
atomics:asgn
hyp1, hyp2:formula
IHhyp1:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp1 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp1 -> formulaDenote atomics f0
IHhyp2:forall (f0 : formula) (known0 : set propvar) (cont0 : set propvar -> bool), forward f0 known0 hyp2 cont0 = true -> (forall known' : set propvar, allTrue atomics known' -> cont0 known' = true -> formulaDenote atomics f0) -> allTrue atomics known0 -> formulaDenote atomics hyp2 -> formulaDenote atomics f0
f:formula
known:set propvar
cont:set propvar -> bool
H:cont known = true
H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics f
H1:allTrue atomics known
H2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2

cont known = true
assumption. Qed.

forall (atomics : asgn) (f : formula) (known : set propvar), backward known f = true -> allTrue atomics known -> formulaDenote atomics f
atomics:asgn
p:propvar
known:set propvar
H:(if in_dec Nat.eq_dec p known then true else false) = true
H0:allTrue atomics known

atomics p
atomics:asgn
known:set propvar
H:false = true
H0:allTrue atomics known
False
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
p:propvar
known:set propvar
i:In p known
H:true = true
H0:allTrue atomics known

atomics p
atomics:asgn
p:propvar
known:set propvar
n:In p known -> False
H:false = true
H0:allTrue atomics known
atomics p
atomics:asgn
known:set propvar
H:false = true
H0:allTrue atomics known
False
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
p:propvar
known:set propvar
i:In p known
H:true = true
H0:allTrue atomics known

allTrue atomics ?s
atomics:asgn
p:propvar
known:set propvar
i:In p known
H:true = true
H0:allTrue atomics known
set_In p ?s
atomics:asgn
p:propvar
known:set propvar
n:In p known -> False
H:false = true
H0:allTrue atomics known
atomics p
atomics:asgn
known:set propvar
H:false = true
H0:allTrue atomics known
False
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
p:propvar
known:set propvar
i:In p known
H:true = true
H0:allTrue atomics known

set_In p known
atomics:asgn
p:propvar
known:set propvar
n:In p known -> False
H:false = true
H0:allTrue atomics known
atomics p
atomics:asgn
known:set propvar
H:false = true
H0:allTrue atomics known
False
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
p:propvar
known:set propvar
i:In p known
H:true = true
H0:allTrue atomics known

In p known
atomics:asgn
p:propvar
known:set propvar
n:In p known -> False
H:false = true
H0:allTrue atomics known
atomics p
atomics:asgn
known:set propvar
H:false = true
H0:allTrue atomics known
False
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
p:propvar
known:set propvar
n:In p known -> False
H:false = true
H0:allTrue atomics known

atomics p
atomics:asgn
known:set propvar
H:false = true
H0:allTrue atomics known
False
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
known:set propvar
H:false = true
H0:allTrue atomics known

False
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known

formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true

formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true

backward ?known f1 = true
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true
allTrue atomics ?known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true

allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 && backward known f2 = true
H0:allTrue atomics known

formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true

formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true

backward ?known f2 = true
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true
allTrue atomics ?known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
H2:backward known f2 = true

allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:backward known f1 || backward known f2 = true
H0:allTrue atomics known

formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true

formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true

formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true

backward ?known f1 = true
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true
allTrue atomics ?known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f1 = true

allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true

formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true

formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true

backward ?known f2 = true
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true
allTrue atomics ?known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H0:allTrue atomics known
H1:backward known f2 = true

allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1

formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1

forward f2 ?known ?hyp ?cont = true
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
forall known' : set propvar, allTrue atomics known' -> ?cont known' = true -> formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
allTrue atomics ?known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics ?hyp
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1

forall known' : set propvar, allTrue atomics known' -> (fun known'0 : set propvar => backward known'0 f2) known' = true -> formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
known':set propvar
H2:allTrue atomics known'
H3:backward known' f2 = true

formulaDenote atomics f2
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
known':set propvar
H2:allTrue atomics known'
H3:backward known' f2 = true

backward ?known f2 = true
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
known':set propvar
H2:allTrue atomics known'
H3:backward known' f2 = true
allTrue atomics ?known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
known':set propvar
H2:allTrue atomics known'
H3:backward known' f2 = true

allTrue atomics known'
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1

allTrue atomics known
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1
formulaDenote atomics f1
atomics:asgn
f1, f2:formula
IHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1
IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2
known:set propvar
H:forward f2 known f1 (fun known' : set propvar => backward known' f2) = true
H0:allTrue atomics known
H1:formulaDenote atomics f1

formulaDenote atomics f1
assumption. Qed.

forall f : formula, backward [] f = true -> forall atomics : asgn, formulaDenote atomics f
f:formula
H:backward [] f = true
atomics:asgn

formulaDenote atomics f
f:formula
H:backward [] f = true
atomics:asgn

backward [] f = true
f:formula
H:backward [] f = true
atomics:asgn
allTrue atomics []
f:formula
H:backward [] f = true
atomics:asgn

allTrue atomics []
<