(8steps total) PrintForm Definitions mb event system 6 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-single-pre-init1-feasible
  T,T':Type, x:Id, c:T, a:Id, P:(TT'Prop).
  T'
  
  (u:T. Dec(v:T'. P(u,v)))
  
  Feasible(ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v)))
By: ProveItFeasible

Generated subgoals:

1 1. T : Type
2. T' : Type
3. Id
4. T
5. a : Id
6. P : TT'Prop
7. T'
8. u:T. Dec(v:T'. P(u,v))
9. k : Knd
10. eqof(KindDeq)(locl(a),k)  false
  Dec(T')
1 step
2 1. T : Type
2. T' : Type
3. x : Id
4. T
5. a : Id
6. P : TT'Prop
7. T'
8. u:T. Dec(v:T'. P(u,v))
9. a@0 : Id
10. eqof(IdDeq)(a,a@0)  false
11. s : State(<[x],x.T>)
  Dec(v:if eqof(KindDeq)(locl(a),locl(a@0))  false T' else Top fi. 
  P(s(x),v))
5 steps
3 1. T : Type
2. T' : Type
3. x : Id
4. T
5. a : Id
6. P : TT'Prop
7. T'
8. u:T. Dec(v:T'. P(u,v))
9. a@0 : Id
10. eqof(IdDeq)(a,a@0)  false
  <[x],x.T>  z:Id fp-> Type
1 step

About:
pairconsnilbfalseifthenelsedecidablelambdaapply
functionuniversemembertoppropimpliesallexists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(8steps total) PrintForm Definitions mb event system 6 Sections EventSystems Search Doc