Nuprl - Pf rel mng 2 wf 1

(16steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1. r: rel()
2. ds: Collection(dec())
3. da: Collection(dec())
4. de: sig()
5. rho: Decl
6. st1: Collection(SimpleType)
7. e: {[[de]] rho}
8. s: {[[ds]] rho}
9. s': {[[ds]] rho}
10. a: [[st1]] rho
11. tr: trace_env([[da]] rho)
12. trace_consistent_rel(rho;da;tr.proj;r)

tc(r;ds;st1;de) list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;r.args) Prop

By: Unfolds [`let`;`tc`] 0 THEN Reduce 0 THEN GenConcl (r.args = l)

Generated subgoal:

1 13. l: Term List
14. r.args = l
Case(r.name) Case eq(Q) = > ||l|| = 2 & Q term_types(ds;st1;de;l[0]) & Q term_types(ds;st1;de;l[1]) Case R = > ||de.rel(R)|| = ||l|| & (i:. i < ||l|| (de.rel(R))[i] term_types(ds;st1;de;l[i])) Default = > False list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;l) Prop

About:

(16steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc