Preuve du théorème

La preuve se fait par induction sur l'expression e :

1. pour les constantes
2. pour les variables                                                                                                         0
3. pour les sommes, en supposant vrai pour les membres de l'addition

1. isconst (e)

outcome (compile(e , t) , R)  =  outcome(mkli (val (e)) , R)        1

                                             =  step (mkli (val(e)) , R)                2

                                             =  a (ac , arg (mkli(val (e))) , R)    3

                                             =  a (ac , val(e) , R)                          4

                                             =  a (ac , value (e , E) , R)              5

                                             =_t a(ac , value (e , E) , R)                6

2. isvar (e)

outcome (compile (e , t) , R)  =  outcome (mkload (loc (e ,map)) , R)                    1

                                             =  step (mkload (loc (e , map)) , R)                            2

                                             =  a (ac , c (adr(mkload (loc (e , map))) , R), R)   3

                                             =  a (ac , c (loc (e , map) , R) , R)                              4

                                             =  a (ac , c (e ,E) , R)                                                  hyp. 3

                                             =  a (ac , value(e , E) , R)                                              5

                                             =_t a(ac , value (e , E) , R)                                              6

3. issum (e)

outcome (compile (e , t) , R)  =  outcome (compile (s1 (e) , t) * mksto (t) * compile (s2(e) , t+1) * mkadd (t) , R)       1

        8                                    = outcome(mkadd (t) ,                          7   trois fois

                                                                outcome (compile(s2 (e) , t + 1) ,

                                                                              outcome (mksto(t) ,

                                                                                             outcome (compile(s1 (e) , t) , R))))

  introduisons des notations :

• v = value (e  , E)
• v₁  = value (s1 (e) , E)               
• v₂  = value (s2 (e) , E)           ->   13      v  = v₁ + v₂    5
• R₁ = outcome (compile (s1 (e) , t) , R)
• R₂ = outcome (mksto (t) , R₁)
• R₃ = outcome (compile (s2 (e) , t + 1) , R₂)
• R₄ = outcome (mkadd (t) , R₃)        ->   R₄ = outcome (compile (e , t) , R)        8

  nous voulons prouver :

R₄ =_t a (ac , v , R)

• R₁ = outcome (compile (s1 (e) , t) , R)            déf. de R₁

11         =_t a (ac , v₁ , R)          ¬  hypothèse d'induction    

c (ac , R₁) = c (ac , a (ac , v₁ , R))

10      v₁  = c (ac , R₁)                                              9

• R₂ = outcome (mksto (t) , R₁)                        déf. de R₂

              =  a (t , c (ac ,  R₁) , R₁)                          3

                      = a (t , v₁ , R₁)                                        10

                      =_{t +1} a (t , v₁ , a (ac , v₁ , R))                  11 + 6

                      =_{t +1,ac} a (t , v₁ , R)                                6

c (t , R₂) = c (t , a (t , v₁ , R))

v₁  = c (t , R₂) 

• R₃ = outcome (compile (s2 (e) , t + 1) , R₂)    déf. de R₃

                     =_{t +1} a (ac , v₂ , R₂)          <-  hypothèse d'induction    

          14        =_{t +1} a (ac , v₂ , a (t , v₁ , R))                    12

        on peut ici utiliser l'hypothèse d'induction car :

            c (loc (v , map) , R₂) = c (loc (v , map) , a (t , v₁ , R)) si loc (v , map) < t

                                            =  c (loc (v , map) , R)  si loc (v , map) < t

                                            = c (v , E)   pour tout v

• R₄ = outcome (mkadd (t) , R₃)                       déf. de R₄

                = step (mkadd (t) , R₃)                                   2

              = a (ac , c (t , R₃) + c (ac , R₃) , R₃)        3

                                     v₁                      v₂ 

              = a (ac , v , R₃)                                       13

              =_{t +1} a (ac , v , a (ac , v₂ , a (t , v₁ , R)))  14

              =_{t +1} a (ac , v , a (t , v₁ , R))                    12

              =_t a (ac , v , R)                                        12

CQFD