| 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 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.prove_even. Qed.isEven 256
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:
forall n n' : nat, n' < n -> if check_even n' then isEven n' else ~ isEven n'n':natH:n' < 0if check_even n' then isEven n' else ~ isEven n'n:natIHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0n':natH:n' < S nif check_even n' then isEven n' else ~ isEven n'n:natIHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0n':natH:n' < S nif check_even n' then isEven n' else ~ isEven n'n:natIHn:forall n' : nat, n' < n -> if check_even n' then isEven n' else ~ isEven n'H:0 < S nisEven 0n:natIHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0n':natH:S n' < S nif match n' with | 0 => false | S n'0 => check_even n'0 end then isEven (S n') else ~ isEven (S n')n:natIHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0n':natH:S n' < S nif match n' with | 0 => false | S n'0 => check_even n'0 end then isEven (S n') else ~ isEven (S n')n:natIHn:forall n' : nat, n' < n -> if check_even n' then isEven n' else ~ isEven n'H:1 < S n~ isEven 1n:natIHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0n':natH:S (S n') < S nif check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))n:natIHn:forall n' : nat, n' < n -> if check_even n' then isEven n' else isEven n' -> FalseH:1 < S nH0:isEven 1Falsen:natIHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0n':natH:S (S n') < S nif check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))n:natIHn:forall n'0 : nat, n'0 < n -> if check_even n'0 then isEven n'0 else ~ isEven n'0n':natH:S (S n') < S nif check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))n, n':natIHn:n' < n -> if check_even n' then isEven n' else ~ isEven n'H:S (S n') < S nif check_even n' then isEven (S (S n')) else ~ isEven (S (S n'))n, n':natHeq:check_even n' = trueIHn:n' < n -> isEven n'H:S (S n') < S nisEven (S (S n'))n, n':natHeq:check_even n' = falseIHn:n' < n -> ~ isEven n'H:S (S n') < S n~ isEven (S (S n'))n, n':natHeq:check_even n' = trueIHn:n' < n -> isEven n'H:S (S n') < S nisEven n'n, n':natHeq:check_even n' = falseIHn:n' < n -> ~ isEven n'H:S (S n') < S n~ isEven (S (S n'))n, n':natHeq:check_even n' = trueIHn:n' < n -> isEven n'H:S (S n') < S nn' < nn, n':natHeq:check_even n' = falseIHn:n' < n -> ~ isEven n'H:S (S n') < S n~ isEven (S (S n'))n, n':natHeq:check_even n' = falseIHn:n' < n -> ~ isEven n'H:S (S n') < S n~ isEven (S (S n'))n, n':natHeq:check_even n' = falseIHn:n' < n -> isEven n' -> FalseH:S (S n') < S nH0:isEven (S (S n'))Falsen, n':natHeq:check_even n' = falseIHn:n' < n -> isEven n' -> FalseH:S (S n') < S nH2:isEven n'Falsen, n':natHeq:check_even n' = falseIHn:n' < n -> isEven n' -> FalseH:S (S n') < S nH2:isEven n'n' < nn, n':natHeq:check_even n' = falseIHn:n' < n -> isEven n' -> FalseH:S (S n') < S nH2:isEven n'isEven n'assumption. Qed.n, n':natHeq:check_even n' = falseIHn:n' < n -> isEven n' -> FalseH:S (S n') < S nH2:isEven n'isEven n'
forall n : nat, check_even n = true -> isEven nn:natH:check_even n = trueisEven nn:natH:check_even n = trueH0:n < S nisEven nn:natH:check_even n = trueH0:if check_even n then isEven n else ~ isEven nisEven nassumption. Qed.n:natH:check_even n = trueH0:isEven nisEven n
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.prove_even_reflective. Qed.isEven 256
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 255Abort.isEven 255
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.
We might also like to have reflective proofs of trivial tautologies like this one:
tauto. Qed.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.
induct t; simplify; propositional. Qed.forall t : taut, tautDenote t
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.
obvious. Qed.True /\ True -> True \/ True /\ (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.
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.
induction ml1; simplify; equality. Qed. Hint Rewrite flatten_correct'.A:Sete:Af:A -> A -> Aassoc:forall a b c : A, a + b + c = a + (b + c)identl:forall a : A, e + a = aidentr:forall a : A, a + e = aforall ml2 ml1 : list A, mldenote (ml1 ++ ml2) = mldenote ml1 + mldenote ml2induction me; simplify; equality. Qed.A:Sete:Af:A -> A -> Aassoc:forall a b c : A, a + b + c = a + (b + c)identl:forall a : A, e + a = aidentr:forall a : A, a + e = aforall me : mexp, mdenote me = mldenote (flatten me)
Now it is easy to prove a theorem that will be the main tool behind our simplification tactic.
simplify; repeat rewrite flatten_correct; assumption. Qed.A:Sete:Af:A -> A -> Aassoc:forall a b c : A, a + b + c = a + (b + c)identl:forall a : A, e + a = aidentr:forall a : A, a + e = aforall me1 me2 : mexp, mldenote (flatten me1) = mldenote (flatten me2) -> mdenote me1 = mdenote me2
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:Sete:Af:A -> A -> Aassoc:forall a b c : A, a + b + c = a + (b + c)identl:forall a : A, e + a = aidentr:forall a : A, a + e = aforall a b c d : A, a + b + c + d = a + (b + c) + dA:Sete:Af:A -> A -> Aassoc:forall a0 b0 c0 : A, a0 + b0 + c0 = a0 + (b0 + c0)identl:forall a0 : A, e + a0 = a0identr:forall a0 : A, a0 + e = a0a, b, c, d:Aa + (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.
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.
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) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) (Initial (subtract_sys 5)) (Initial (subtract_sys 5)) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5} {5} ?invariant1forall 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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) ({5} \cup (({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { })) ((({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { }) \setminus {5}) ?invariant1forall 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} ?invariant1forall 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 natconstant ns = constant (dedup ns)e1, e2:setexprIHe1:setexprDenote e1 = constant (normalize e1)IHe2:setexprDenote e2 = constant (normalize e2)setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))ns:list natH:constant (map (fun x : nat => x) (dedup ns)) = constant (map (fun x : nat => x) ns)constant ns = constant (dedup ns)e1, e2:setexprIHe1:setexprDenote e1 = constant (normalize e1)IHe2:setexprDenote e2 = constant (normalize e2)setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))ns:list natH:constant (dedup ns) = constant nsconstant ns = constant (dedup ns)e1, e2:setexprIHe1:setexprDenote e1 = constant (normalize e1)IHe2:setexprDenote e2 = constant (normalize e2)setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))e1, e2:setexprIHe1:setexprDenote e1 = constant (normalize e1)IHe2:setexprDenote e2 = constant (normalize e2)setexprDenote e1 \cup setexprDenote e2 = constant (setmerge (normalize e1) (normalize e2))e1, e2:setexprIHe1: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:setexprIHe1: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))equality. Qed.e1, e2:setexprIHe1: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))
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) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) (Initial (subtract_sys 5)) (Initial (subtract_sys 5)) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5} {5} ?invariant1forall 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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) ({5} \cup (({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { })) ((({5} \cup ({4} \cup ({3} \cup ?rest))) \cup { }) \setminus {5}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3} ((({5} \cup ({4} \cup ({3} \cup { }))) \cup { }) \setminus {5}) ?invariant1forall 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}) ?invariant1forall 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} ?invariant1forall s : nat, ?invariant1 s -> s <= 5oneStepClosure (subtract_sys 5) {4, 3} ?inv'multiStepClosure (subtract_sys 5) ({5, 4, 3} \cup ?inv') (?inv' \setminus {5, 4, 3}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1} ({4, 3, 2, 1} \setminus {5, 4, 3}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1} {2, 1} ?invariant1forall s : nat, ?invariant1 s -> s <= 5oneStepClosure (subtract_sys 5) {2, 1} ?inv'multiStepClosure (subtract_sys 5) ({5, 4, 3, 2, 1} \cup ?inv') (?inv' \setminus {5, 4, 3, 2, 1}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} ({2, 1, 0} \setminus {5, 4, 3, 2, 1}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} {0} ?invariant1forall s : nat, ?invariant1 s -> s <= 5oneStepClosure (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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (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}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} ((({0} \cup { }) \cup { }) \setminus {5, 4, 3, 2, 1, 0}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} ({0} \setminus {5, 4, 3, 2, 1, 0}) ?invariant1forall s : nat, ?invariant1 s -> s <= 5multiStepClosure (subtract_sys 5) {5, 4, 3, 2, 1, 0} { } ?invariant1forall s : nat, ?invariant1 s -> s <= 5forall s : nat, {5, 4, 3, 2, 1, 0} s -> s <= 5linear_arithmetic. Qed.s:natH:5 = s \/ 4 = s \/ 3 = s \/ 2 = s \/ 1 = s \/ 0 = s \/ Falses <= 5
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.
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.induct s; simplify; propositional; match goal with | [ |- context[if ?E then _ else _] ] => destruct E end; simplify; propositional. Qed.atomics:asgnforall (v : nat) (s : set propvar), allTrue s -> atomics v -> allTrue (add s v)induct s; simplify; equality. Qed.atomics:asgnforall (v : propvar) (s : set propvar), allTrue s -> set_In v s -> atomics v
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 fatomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics pformulaDenote atomics fatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:TrueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics pallTrue atomics (add known p)atomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics pcont (add known p) = trueatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:TrueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics pallTrue atomics knownatomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics patomics patomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics pcont (add known p) = trueatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:TrueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics patomics patomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics pcont (add known p) = trueatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:TrueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnp:propvarf:formulaknown:set propvarcont:set propvar -> boolH:cont (add known p) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:atomics pcont (add known p) = trueatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:TrueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:TrueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:TrueallTrue atomics ?known'atomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:Truecont ?known' = trueatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnf:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:Truecont known = trueatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:formulaDenote atomics (Imp hyp2 f)H0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2forall known' : set propvar, allTrue atomics known' -> forward f known' hyp2 cont = true -> formulaDenote atomics (Imp hyp2 f)atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2forall known' : set propvar, allTrue atomics known' -> forward f known' hyp2 cont = true -> formulaDenote atomics (Imp hyp2 f)atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2forward f ?known hyp2 ?cont = trueatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2forall known'0 : set propvar, allTrue atomics known'0 -> ?cont known'0 = true -> formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2allTrue atomics ?knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2formulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2allTrue atomics known'atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2formulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2allTrue atomics known'atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2formulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known'0 : set propvar => forward f known'0 hyp2 cont) = trueH0:forall known'0 : set propvar, allTrue atomics known'0 -> cont known'0 = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2known':set propvarH2:allTrue atomics known'H5:forward f known' hyp2 cont = trueH6:formulaDenote atomics hyp2formulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2allTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward (Imp hyp2 f) known hyp1 (fun known' : set propvar => forward f known' hyp2 cont) = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H4:formulaDenote atomics hyp2formulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueforward f ?known hyp1 ?cont = trueatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueforall known' : set propvar, allTrue atomics known' -> ?cont known' = true -> formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueallTrue atomics ?knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueforall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueallTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueallTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp1H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp1atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:forward f known hyp1 cont && forward f known hyp2 cont = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueforward f ?known hyp2 ?cont = trueatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueforall known' : set propvar, allTrue atomics known' -> ?cont known' = true -> formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueallTrue atomics ?knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueforall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueallTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueallTrue atomics knownatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH3:formulaDenote atomics hyp2H2:forward f known hyp1 cont = trueH4:forward f known hyp2 cont = trueformulaDenote atomics hyp2atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2formulaDenote atomics fatomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2allTrue atomics ?known'atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2cont ?known' = trueassumption. Qed.atomics:asgnhyp1, hyp2:formulaIHhyp1: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 f0IHhyp2: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 f0f:formulaknown:set propvarcont:set propvar -> boolH:cont known = trueH0:forall known' : set propvar, allTrue atomics known' -> cont known' = true -> formulaDenote atomics fH1:allTrue atomics knownH2:formulaDenote atomics hyp1 -> formulaDenote atomics hyp2cont known = trueforall (atomics : asgn) (f : formula) (known : set propvar), backward known f = true -> allTrue atomics known -> formulaDenote atomics fatomics:asgnp:propvarknown:set propvarH:(if in_dec Nat.eq_dec p known then true else false) = trueH0:allTrue atomics knownatomics patomics:asgnknown:set propvarH:false = trueH0:allTrue atomics knownFalseatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnp:propvarknown:set propvari:In p knownH:true = trueH0:allTrue atomics knownatomics patomics:asgnp:propvarknown:set propvarn:In p known -> FalseH:false = trueH0:allTrue atomics knownatomics patomics:asgnknown:set propvarH:false = trueH0:allTrue atomics knownFalseatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnp:propvarknown:set propvari:In p knownH:true = trueH0:allTrue atomics knownallTrue atomics ?satomics:asgnp:propvarknown:set propvari:In p knownH:true = trueH0:allTrue atomics knownset_In p ?satomics:asgnp:propvarknown:set propvarn:In p known -> FalseH:false = trueH0:allTrue atomics knownatomics patomics:asgnknown:set propvarH:false = trueH0:allTrue atomics knownFalseatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnp:propvarknown:set propvari:In p knownH:true = trueH0:allTrue atomics knownset_In p knownatomics:asgnp:propvarknown:set propvarn:In p known -> FalseH:false = trueH0:allTrue atomics knownatomics patomics:asgnknown:set propvarH:false = trueH0:allTrue atomics knownFalseatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnp:propvarknown:set propvari:In p knownH:true = trueH0:allTrue atomics knownIn p knownatomics:asgnp:propvarknown:set propvarn:In p known -> FalseH:false = trueH0:allTrue atomics knownatomics patomics:asgnknown:set propvarH:false = trueH0:allTrue atomics knownFalseatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnp:propvarknown:set propvarn:In p known -> FalseH:false = trueH0:allTrue atomics knownatomics patomics:asgnknown:set propvarH:false = trueH0:allTrue atomics knownFalseatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnknown:set propvarH:false = trueH0:allTrue atomics knownFalseatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = trueformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = truebackward ?known f1 = trueatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = trueallTrue atomics ?knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = trueallTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 && backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = trueformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = truebackward ?known f2 = trueatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = trueallTrue atomics ?knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueH2:backward known f2 = trueallTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:backward known f1 || backward known f2 = trueH0:allTrue atomics knownformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueformulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = truebackward ?known f1 = trueatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueallTrue atomics ?knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f1 = trueallTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueformulaDenote atomics f1 \/ formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = truebackward ?known f2 = trueatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueallTrue atomics ?knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH0:allTrue atomics knownH1:backward known f2 = trueallTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1forward f2 ?known ?hyp ?cont = trueatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1forall known' : set propvar, allTrue atomics known' -> ?cont known' = true -> formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1allTrue atomics ?knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics ?hypatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1forall known' : set propvar, allTrue atomics known' -> (fun known'0 : set propvar => backward known'0 f2) known' = true -> formulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1allTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1known':set propvarH2:allTrue atomics known'H3:backward known' f2 = trueformulaDenote atomics f2atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1allTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1known':set propvarH2:allTrue atomics known'H3:backward known' f2 = truebackward ?known f2 = trueatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1known':set propvarH2:allTrue atomics known'H3:backward known' f2 = trueallTrue atomics ?knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1allTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known'0 : set propvar => backward known'0 f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1known':set propvarH2:allTrue atomics known'H3:backward known' f2 = trueallTrue atomics known'atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1allTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f1atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1allTrue atomics knownatomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f1assumption. Qed.atomics:asgnf1, f2:formulaIHf1:forall known0 : set propvar, backward known0 f1 = true -> allTrue atomics known0 -> formulaDenote atomics f1IHf2:forall known0 : set propvar, backward known0 f2 = true -> allTrue atomics known0 -> formulaDenote atomics f2known:set propvarH:forward f2 known f1 (fun known' : set propvar => backward known' f2) = trueH0:allTrue atomics knownH1:formulaDenote atomics f1formulaDenote atomics f1forall f : formula, backward [] f = true -> forall atomics : asgn, formulaDenote atomics ff:formulaH:backward [] f = trueatomics:asgnformulaDenote atomics ff:formulaH:backward [] f = trueatomics:asgnbackward [] f = truef:formulaH:backward [] f = trueatomics:asgnallTrue atomics []f:formulaH:backward [] f = trueatomics:asgnallTrue atomics []propositional. Qed.f:formulaH:backward [] f = trueatomics:asgnTrue
Find the position of an element in a list.
Ltac position x ls :=
match ls with
| [] => constr:(@None nat)
| x :: _ => constr:(Some 0)
| _ :: ?ls' =>
let p := position x ls' in
match p with
| None => p
| Some ?n => constr:(Some (S n))
end
end.Compute a duplicate-free list of all variables in P, combining it with acc.
Ltac vars_in P acc :=
match P with
| True => acc
| False => acc
| ?Q1 /\ ?Q2 =>
let acc' := vars_in Q1 acc in
vars_in Q2 acc'
| ?Q1 \/ ?Q2 =>
let acc' := vars_in Q1 acc in
vars_in Q2 acc'
| ?Q1 -> ?Q2 =>
let acc' := vars_in Q1 acc in
vars_in Q2 acc'
| _ =>
let pos := position P acc in
match pos with
| Some _ => acc
| None => constr:(P :: acc)
end
end.Reification of formula P, with a pregenertaed list vars of variables it may mention
Ltac reify_tauto' P vars :=
match P with
| True => Truth
| False => Falsehood
| ?Q1 /\ ?Q2 =>
let q1 := reify_tauto' Q1 vars in
let q2 := reify_tauto' Q2 vars in
constr:(And q1 q2)
| ?Q1 \/ ?Q2 =>
let q1 := reify_tauto' Q1 vars in
let q2 := reify_tauto' Q2 vars in
constr:(Or q1 q2)
| ?Q1 -> ?Q2 =>
let q1 := reify_tauto' Q1 vars in
let q2 := reify_tauto' Q2 vars in
constr:(Imp q1 q2)
| _ =>
let pos := position P vars in
match pos with
| Some ?pos' => constr:(Atomic pos')
end
end.Our final tactic implementation is now fairly straightforward. First, we intro all quantifiers that do not bind Props. Then we reify. Finally, we call the verified procedure through a lemma.
Ltac my_tauto :=
repeat match goal with
| [ |- forall x : ?P, _ ] =>
match type of P with
| Prop => fail 1
| _ => intro
end
end;
match goal with
| [ |- ?P ] =>
let vars := vars_in P (@nil Prop) in
let p := reify_tauto' P vars in
change (formulaDenote (nth_default False vars) p)
end;
apply backward_ok; reflexivity.A few examples demonstrate how the tactic works:
my_tauto. Qed.Truemy_tauto. Qed.forall x y : nat, x = y -> x = y
Crucially, both instances of x = y are represented with the same variable 0.
my_tauto. Qed.forall x y z : nat, x < y /\ y > z \/ y > z /\ x < S y -> y > z /\ (x < y \/ x < S y)
Our goal contained three distinct atomic formulas, and we see that a three-element environment is generated.
It can be interesting to observe differences between the level of repetition in proof terms generated by my_tauto and tauto for especially trivial theorems.
my_tauto. Qed.True /\ True /\ True /\ True /\ True /\ True /\ False -> Falsetauto. Qed.True /\ True /\ True /\ True /\ True /\ True /\ False -> False
The traditional tauto tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by my_tauto always have linear size.