Nuprl - Pf trivial_term

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

t:Term, as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t)

By: Analyze 0 THEN TermInd 1 THEN Unfold `term_subst` 0 THEN Reduce 0 THEN Try (Fold `term_subst` 0) THEN Try ((RW (AddrC [3] (UnfoldC `unprime`)) 0) THEN (Reduce 0) THEN (Complete SmAuto)) THEN Try ((Unfold `unprime` 0) THEN (Reduce 0) THEN (Fold `unprime` 0) THEN Analyze THEN SmAuto)

Generated subgoal:

1 1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t)
4. x: Label
5. as: (LabelTerm) List
6. x:Label. unprime(apply_alist(as;x;x)) = x
unprime(apply_alist(as;x;x')) = unprime(x')

About:

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