r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc(rel_unprime(r);ds;da;de)

Auto
THEN
All (Unfolds [`tc`;`rel_unprime`])
THEN
Analyze 1
THEN
Analyze 1
THEN
All Reduce
THEN
ExRepD
THEN
Analyze 0
THEN
Try (All (RWW "map_length_nat"))
THEN
All (RWW "map_select")
THEN
All Reduce
THEN
Try (RWW "map_length_nat" -1)
THEN
Try (Complete ((Subst (term_types(ds;da;de;unprime(r1[0])) ~ term_types(ds;da;de;r1[0])) 0) THEN (Try Trivial) THEN (Try (BackThru Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)))))
THEN
Try (Complete ((Subst (term_types(ds;da;de;unprime(r1[1])) ~ term_types(ds;da;de;r1[1])) 0) THEN (Try Trivial) THEN (Try (BackThru Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)))))
THEN
Try (Complete ((Subst (term_types(ds;da;de;unprime(r1[i])) ~ term_types(ds;da;de;r1[i])) 0) THEN (Try Trivial) THEN (Try (BackThru Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t))) THEN (Try BackThruSomeHyp)))
THEN
Try (Complete ((Subst (term_types(ds;da;de;unprime(r1[0])) ~ term_types(ds;da;de;r1[0])) -3) THEN (Try Trivial) THEN (Try (BackThru Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)))))
THEN
Try (Complete ((Subst (term_types(ds;da;de;unprime(r1[1])) ~ term_types(ds;da;de;r1[1])) -2) THEN (Try Trivial) THEN (Try (BackThru Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)))))
THEN
Try (Complete ((All (InstHyp [i])) THEN (Subst (term_types(ds;da;de;unprime(r1[i])) ~ term_types(ds;da;de;r1[i])) -1) THEN (Try Trivial) THEN (Try (BackThru Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t))) THEN (Try BackThruSomeHyp)))
THEN
Try (Complete Auto)
THEN
AllHyps (i.(Unfold `ioa_mng` i) THEN (Reduce i) THEN Trivial)
THEN
Try ((BackThru Thm* v:Top, rho:Decl. v [[ < > ]] rho) THEN Trivial)

None

About: