At: covers pred addprime2 1. Q: Fmla 2. A: ioa{i:l}() 3. x:Label. (r:rel(). r Q & (i:. i < ||r.args|| & (x term_vars(r.args[i])))) covers_var(A;x) 4. x: Label 5. r: rel() 6. r@0: rel() 7. r@0 Q 8. r = mk_rel(r@0.name, map(t.(t)';r@0.args)) 9. i: 10. i < ||r@0.args|| 11. (x term_vars((r@0.args[i])'))
(x term_vars(r@0.args[i])) By: MoveToConcl -1
THEN
GenConcl (r@0.args[i] = t)
THEN
Thin -1
THEN
TermInd -1
THEN
Unfold `addprime` 0
THEN
Reduce 0
THEN
Try (Complete Auto)
THEN
Try (Fold `addprime` 0)
THEN
RWO "member_append" 0
THEN
ParallelOp -1
THEN
EasyHyp Generated subgoals:
x:Label. (
r:rel(). r 
Q & (
. i < ||r.args|| & (x 
covers_var(A;x)
t.(t)';r@0.args))
(x