Go backward to Record Introduction Principle Go up to Top Go forward to Summary (Semantics) |
pi |- D: pi1dec | pi -U- pi1 |- U: theta |
pi |- begin D in U end: theta |
pi |- D1: pi1dec | pi -U- pi1 |- D2: pi2dec |
pi |- begin D in D2 end: pi2dec |
pi |- D: pi1dec | pi -U- pi1 |- T: deltaclass |
pi |- begin D in T end: deltaclass |
pi |- D: pi1dec | pi -U- pi1 |- C: comm |
pi |- begin D in C end: comm |
pi |- D: pi1dec | pi -U- pi1 |- E: tauexp |
pi |- begin D in E end: tauexp |