Nuprl - Pf rel_mng_2

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

1. name: relname()
2. r1: Term List
3. rho: Top
4. ds: Top
5. da: Top
6. de: Top
7. e: Top
8. s: Top
9. s': Top
10. a: Top
11. tr: Top
12. u: Term
13. v: Term List
14. z:Top. list_accum(x,t.x([[t]] 1of(e) s s' a tr);z;map(t. unprime(t);v)) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);z;v)
15. z: Top

list_accum(x,t.x([[t]] 1of(e) s s' a tr);z([[unprime(u)]] 1of(e) s s' a tr);map(t. unprime(t);v)) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);z([[u]] 1of(e) s a tr);v)

By: Subst ([[unprime(u)]] 1of(e) s s' a tr ~ [[u]] 1of(e) s a tr) 0 THEN Try (BackThru Thm* t:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a tr) THEN Try BackThruSomeHyp

Generated subgoals:

None

About:

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