Nuprl - Pf rel_mentions_trace

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

1. r: rel()

reduce(x,y. mentions_trace(x) y;false;r.args) (i:. i < ||r.args|| & mentions_trace(r.args[i]))

By: GenConcl (r.args = L) THEN Thin -1 THEN ListInd -1 THEN Reduce 0 THEN ExRepD THEN All (RW assert_pushdownC)

Generated subgoals:

1 2. L: Term List
3. u: Term
4. v: Term List
5. reduce(x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i]))
6. reduce(x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i]))
7. mentions_trace(u) reduce(x,y. mentions_trace(x) y;false;v)
i:. i < ||v||+1 & mentions_trace([u / v][i])

2 2. L: Term List
3. u: Term
4. v: Term List
5. reduce(x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i]))
6. reduce(x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i]))
7. i:
8. i < ||v||+1
9. mentions_trace([u / v][i])
mentions_trace(u) reduce(x,y. mentions_trace(x) y;false;v)

About:

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

1	2. `L:` `Term List` 3. `u:` `Term` 4. `v:` `Term List` 5. `reduce(x,y. mentions_trace(x) y;false;v) (i:. i < \|\|v\|\| & mentions_trace(v[i]))` 6. `reduce(x,y. mentions_trace(x) y;false;v) (i:. i < \|\|v\|\| & mentions_trace(v[i]))` 7. `mentions_trace(u) reduce(x,y. mentions_trace(x) y;false;v)` `i:. i < \|\|v\|\|+1 & mentions_trace([u / v][i])`
2	2. `L:` `Term List` 3. `u:` `Term` 4. `v:` `Term List` 5. `reduce(x,y. mentions_trace(x) y;false;v) (i:. i < \|\|v\|\| & mentions_trace(v[i]))` 6. `reduce(x,y. mentions_trace(x) y;false;v) (i:. i < \|\|v\|\| & mentions_trace(v[i]))` 7. `i:` 8. `i < \|\|v\|\|+1` 9. `mentions_trace([u / v][i])` `mentions_trace(u) reduce(x,y. mentions_trace(x) y;false;v)`