[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Proof step 10 from proof valid-eraseqd-nodups1 (
previous step
)
valid-eraseq(q + q1), m ∈ q1, m ∈ q, ∀ q0, m0. ¬ valid-eraseq(q + q0) ∨ ¬ m0 ∈ q0 ∨ ¬ m0 ∈ q ⊦ m1 ∈ q, m1 ∈ q1
Heuristic quantifier closing applied rule all left
And closed the goal!
Rule argument
pos: left 4 terms: q1, m
Additional information
Used terms: q1, m