Exercice 1
----------

[
  FUN f int [x:bool,y:int](if x y 0);
  ECHO ([b:bool](f b 42) true)
]

G0 |-{dec} (FUN f int [x:bool,y:int](if x y 0)) : G0[f:bool->int->int]
par (FUN)
- G0[x:bool,y:int] |-{exp} (if x y 0) : int
  par (IF)
  - G0[x:bool,y:int] |-{exp} x : bool par (ID).
  - G0[x:bool,y:int] |-{exp} y : int  par (ID).
  - G0[x:bool,y:int] |-{exp} 0 : int  par (NUM).

soit G = G0[f: bool -> int -> int]
G |-{stat} ECHO ([b:bool](f b 42) true) : void
par (echo)
- G |-{exp} ([b:bool](f b 42) true) : int
  par (APP)
  - G |-{exp} [b:bool](f b 42) : bool -> int
    par (ABS)
    - G[b:bool] |-{exp} (f b 42) : int
      par (APP)
      - G[b:bool] |-{exp} f : bool -> int -> int par (ID).
      - G[b:bool] |-{exp} b : bool par (ID).
      - G[b:bool] |-{exp} 42 : int par (NUM).
  - G |-  true : bool par (ID) G(true)=G0(true)=bool.

Exercice 2:
-----------

[
  CONST x int 42;
  FUN f [x:bool](if x 0 1);
  ECHO (add x (f true))
]


|-{dec} CONST x int 42 ~> [x=inZ(42)] par (CONST).

[x=inZ(42)]|-{dec} FUN f [x:bool](if x 0 1)
                   ~> [x=inZ(42),f=InF((if x 0 1),\v.[x=inZ(42);x=v])] par (FUN)

soit r1 =[x=inZ(42),f=InF((if x 0 1),\v.[x=inZ(42);x=v])]
r1,$ |-{stat} ECHO (add x (f bool)) ~> (42.$)
par (ECHO)
- r1 |- (add x (f bool)) ~> inZ(42)
  par (PRIM2)
  - r1 |- x ~> inZ(42)
    par (ID)
    - r1(x) = [x=inZ(42);f=inF(..)](x) = [x=inZ(42)](x) = inZ(42).
  - r1 |- (f true) ~> inZ(0)
    par (APP)
    - r1 |- f ~> inF((if x 0 1),\v.[x=inZ(42);x=v]).
    - r1 |- false ~> inZ(0) par (FALSE).
    - r2 = \v.[x=inZ(42);x=v](inZ(0)) = [x=inZ(42);x=inZ(0)]
      r2 |- (if x 0 1) ~> inZ(0)
      par (IF0)
      - r2 |- x ~> inZ(0) par (ID) r2(x) = [x=inZ(42),x=inZ(0)](x) = inZ(0).
      - r2 |- 0 ~> inZ(0) par (NUM).
  - pi(add)(42,0) = 42+0 = 42
 
Exercice 3:
-----------

Soit phi = \v1.inF((if x 42 (f (not x))),\v2.[x=v2][f=v1]
Soit r = [f=inFR(phi)]

r |- (f false) ~> inZ(42)
par (APPR)
- r |- f ~> inFR(phi).
- r |- false ~> inZ(0) par (FALSE).
- phi(inFR(phi)) = inF((if x 42 (f (not x))),\v2.[x=v2][f=phi])
  r1 = \v2.[x=v2][f=phi](inZ(0)) = [x=inZ(0)][f=phi]
  r1 |- (if x 42 (f (not x))) ~> inZ(42)
  par (IF0)
  - r1 |- x ~> inZ(0) par (ID).
  - r1 |- (f (not x)) ~> inZ(42)
    par (APPR)
    - r1 |- f ~> inFR(phi).
    - r1 |- (not x) ~> inZ(1)
      par (PRIM1)
      - r1 |- x ~> inZ(0) par (ID).
      - pi(not)(0) = 1.
    - phi(inFR(phi)) = inF((if x 42 (f (not x))),\v2.[x=v2][f=inFR(phi)])
      r3 = \v2.[x=v2][f=inFR(phi)](inZ(0))
         = [x=inZ(0)][f=inFR(phi)]
      r3 |- (if x 42 (f (not x))) ~> inZ(42)
      par (IF1)
      - r3 |- x ~> inZ(1) par (ID).
      - r3 |- 42 ~> inZ(42) par (NUM).