Full Language (Contd)

pi |- E$$1: tauexp	pi |- E$$2: tauexp
pi |- E$$1=E$$2: boolexp

pi |- E: boolexp

pi |- not E: boolexp

pi |- E: intloc

pi |- @E: intexp

pi |- N: intexp

pi |- L: intloc

pi |- E: theta

pi |- I=E: {I:theta}

pi |- E$$1: pi$$1	pi |- E$$2: pi$$2
pi |- E$$1,E$$2: pi$$1 U pi$$2

pi |- E$$1: pi$$1	pi -U- pi$$1 |- E$$2: theta
pi |- with E$$1 do E$$2: theta

pi |- I: theta

if (I:theta) in pi

pi -U- {I:theta$$1} |- E:theta$$2

pi |- lambdaI:theta$$1. E: theta$$1 $->$ theta$$2

pi |- E$$1: theta$$1 $->$ theta$$2	pi |- E$$2: theta$$1
pi |- E$$1 E$$2: theta$$2

pi |- I: theta

if (I:theta) in pi