Nuprl - Pf term mng tappend

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

u:Term, d:Decl, tr:trace_env(d), a:(d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr)

By: Analyze 0 THEN TermInd 1 THEN Reduce 0 THEN Try (Complete Auto)

Generated subgoals:

1 1. u: Term
2. u1: TermType{i'}
3. w: u:{v:Term| u1(v) }d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr)
4. y1: Label
d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. tr.proj(y1,kind(a)) (tappend(tr;a).y1 ~ tr.y1)

2 1. u: Term
2. u1: TermType{i'}
3. w: u:{v:Term| u1(v) }d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr)
4. y1: {v:Term| u1(v) }
5. y2: {v:Term| u1(v) }
d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. (affects_trace(tr.proj;kind(a);y1) affects_trace(tr.proj;kind(a);y2)) (([[y1]] e s v tappend(tr;a)([[y2]] e s v tappend(tr;a))) ~ ([[y1]] e s v tr([[y2]] e s v tr)))

About:

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