Nuprl - Pf covers_pred

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q)

By: Unfolds [`covers_pred`;`pred_addprime`] 0 THEN Try ((Unfold `pred` 0) THEN (Fold `pred` 0)) THEN All (RW ColMemberC) THEN Try BackThruSomeHyp THEN All (Unfold `pred_mentions`) THEN All (RW ColMemberC) THEN ExRepD THEN Try ((InstConcl [r@0]) THEN (Try (Fold `pred` 0)) THEN (HypSubst -2 -1)) THEN Try ((InstConcl [(r)']) THEN (Try (AutoInstConcl [])) THEN (Try (Fold `pred` 0))) THEN All (Unfolds [`rel_addprime`;`rel_mentions`]) THEN ExRepD THEN InstConcl [i] THEN All Reduce THEN All (i.RWW "map_length_nat" i) THEN All (i.(RWW "map_select" i) THEN (Reduce i))

Generated subgoals:

1 1. Q: Fmla
2. A: ioa{i:l}()
3. x:Label. (r:rel(). (r@0:rel(). r@0 Q & r = mk_rel(r@0.name, map(t.(t)';r@0.args))) & (i:. i < ||r.args|| & (x term_vars(r.args[i])))) covers_var(A;x)
4. x: Label
5. r: rel()
6. r Q
7. i:
8. i < ||r.args||
9. (x term_vars(r.args[i]))
(x term_vars((r.args[i])'))

2 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]))

About:

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1	1. `Q:` `Fmla` 2. `A:` `ioa{i:l}()` 3. `x:Label. (r:rel(). (r@0:rel(). r@0 Q & r = mk_rel(r@0.name, map(t.(t)';r@0.args))) & (i:. i < \|\|r.args\|\| & (x term_vars(r.args[i])))) covers_var(A;x)` 4. `x:` `Label` 5. `r:` `rel()` 6. `r Q` 7. `i:` 8. `i < \|\|r.args\|\|` 9. `(x term_vars(r.args[i]))` `(x term_vars((r.args[i])'))`
2	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]))`