Langage source

• isconst (e)                                        val (e)

• isvar (e)                                            c (e , E)

• issum (e)  -> s1 (e)   s2 (e)

Sémantique :

    value (e,E) = if         isconst (e)   then   val (e)

           5             elseif   isvar (e)       then   c (e , E)

                          elseif   issum (e)      then 

                                                          value ( s1(e) , x) + value ( s2 (e) , E)

E : environnement

d'où une induction :

0  Si isconst (e) implique P(e) et

        isvar (e) implique P (e) et

         issum (e) implique (P (s1 (e)) et P (s2 (e))) qui implique P (e)

    Alors pour toute e on a P (e).