1. i : Id
2. x : Id
3. y : Id
4. k : Knd
5. T : Type
6. A : Type
7. B : Type
8. f : ABTA
9. y = x
10. x : A  y : B  x:Id fp-> Type
11. k : T  k:Knd fp-> Type
12. @i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))
12.  Dsys
12. & (D:Dsys. 
12. & (@i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v))
12. & (@i: ma-single-effect()  D
12. & (
12. & (D 
12. & (realizes es.(x@0:Id. vartype(i;x@0) r x : A  y : B(x@0)?Top)
12. & (realizes es.& (e:E. 
12. & (realizes es.& (loc(e) = i  (valtype(e) r ma-valtype(k : T; kind(e))))
12. & (realizes es.& (e:E. 
12. & (realizes es.& (loc(e) = i
12. & (realizes es.& (
12. & (realizes es.& (kind(e) = k
12. & (realizes es.& (
12. & (realizes es.& ((x after e)
12. & (realizes es.& (=
12. & (realizes es.& ((s,v. f(s(x),s(y),v))((z.(z when e)),val(e))))
  @i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))
   Dsys
  & (D:Dsys. 
  & (@i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v))
  & (@i: ma-single-effect()  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = k  Knd
  & (realizes es.& (
  & (realizes es.& ((x after e) = f((x when e),(y when e),val(e))  A))

By:

ExRepD THEN BetterSplitAndConcl THEN Try Trivial THEN All Reduce THEN ParallelOp -2 THEN RepeatFor 7 (ParallelOp -1) THEN Unfold `ma-valtype` -1 THEN Reduce -1 THEN ExRepD THEN BetterSplitAndConcl THEN Try Trivial THEN AllHyps (h.InstHyp [x] h THENA Complete Auto THEN ReduceFpf -1 THEN Complete Auto) THEN AllHyps (h. (InstHyp [y] h THENA Complete Auto THEN ReduceFpf -1 THEN SplitOnHypITE -1 (THEN (AllHyps (h.Analyze h THEN Complete Auto) (THEN (Trivial) THEN AllHyps (h. (ParallelOp h THEN ThinTrivial THEN WeakSubstFor kind(e) -1 THEN Reduce -1 (THEN (Complete Auto) THEN AllHyps (h.ReduceFpf h THEN Trivial)

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html