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

At: rel arg typing


r:rel(), i:, ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) i < ||r.args|| [[r.args[i]]] e s a tr [[rel_arg_typ(r.name;i;de)]] rho

By:
Unfolds [`tc`;`rel_arg_typ`] 0
THEN
Analyze 0
THEN
Analyze 1
THEN
Analyze 1
THEN
Reduce 0
THEN
Try ((Fold `mk_rel` 0) THEN (Folds [`relname_other`;`relname_eq`] 0))
THEN
ExRepD
THEN
Using [`de',de] (BackThru Thm* ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent(rho;da;tr.proj;t) a term_types(ds;st1;de;t) [[t]] e s v tr [[a]] rho)
THEN
SmAuto
THEN
AllHyps (h.(Unfold `trace_consistent_rel` h) THEN (Reduce h) THEN (InstHyp [i] h) THEN (Complete Auto))


Generated subgoal:

11. x: SimpleType
2. r1: Term List
3. i:
4. ds: Collection(dec())
5. da: Collection(dec())
6. st1: Collection(SimpleType)
7. de: sig()
8. rho: Decl
9. s: {[[ds]] rho}
10. e: {1of([[de]] rho)}
11. a: [[st1]] rho
12. tr: trace_env([[da]] rho)
13. trace_consistent_rel(rho;da;tr.proj; < inl(x),r1 > )
14. ||r1|| = 2
15. x term_types(ds;st1;de;r1[0])
16. x term_types(ds;st1;de;r1[1])
17. i < ||r1||
x term_types(ds;st1;de;r1[i])

About:
less_thanmemberimpliesall

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