matita/matita/contribs/assembly/compiler/astfe_to_linearfe.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "compiler/linearfe.ma".
  23
  24 (* ***************************** *)
  25 (* PASSO 3 : da ASTFE a LINEARFE *)
  26 (* ***************************** *)
  27
  28 (*
  29   ASTFE_STM_ASG: ∀t:ast_type.
  30                  astfe_var e false t → astfe_expr e t → astfe_stm e
  31 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
  32                   astfe_id e b t → astfe_init e t → astfe_stm e
  33 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
  34 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
  35 *)
  36 inductive astfe_to_linearfe_stm_record (fe:aux_flatEnv_type) : Type ≝
  37   ASTFE_TO_LINEARFE_STM_RECORD_SINGLE: linearfe_stm fe → astfe_to_linearfe_stm_record fe
  38 | ASTFE_TO_LINEARFE_STM_RECORD_MULTI: nat → jumpBlock fe → linearfe_prog fe → astfe_to_linearfe_stm_record fe.
  39
  40 definition defined_astfetolinearfe ≝
  41 λfe.λl:linearfe_prog fe.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
  42
  43 inductive astfe_to_linearfe_stm_record_aux (fe:aux_flatEnv_type) : Type ≝
  44  ASTFE_TO_LINEARFE_STM_RECORD_AUX: nat → ∀prg:linearfe_prog fe.defined_astfetolinearfe fe prg → astfe_to_linearfe_stm_record_aux fe.
  45
  46 lemma append_to_definedAstfetolinearfe :
  47  ∀fe.∀h:linearfe_elem fe.∀t:linearfe_prog fe.
  48   defined_astfetolinearfe fe (cons ? h t).
  49  intros;
  50  simplify;
  51  apply I.
  52 qed.
  53
  54 let rec astfe_to_linearfe_stm fe (ast:astfe_stm fe) (nextL:nat) on ast
  55  : astfe_to_linearfe_stm_record fe ≝
  56  match ast with
  57   [ ASTFE_STM_ASG sType sVar sExpr ⇒
  58    ASTFE_TO_LINEARFE_STM_RECORD_SINGLE fe (LINEARFE_STM_ASG fe sType sVar sExpr)
  59
  60   | ASTFE_STM_INIT sB sType sId sInit ⇒
  61    ASTFE_TO_LINEARFE_STM_RECORD_SINGLE fe (LINEARFE_STM_INIT fe sB sType sId sInit)
  62
  63   | ASTFE_STM_WHILE sExpr sBody ⇒
  64   (* while(EXP) { ... } diventa if(EXP) { do { ... } while (EXP); } *)
  65    match astfe_to_linearfe_body fe sBody (S nextL) (JUMPBLOCK_COND fe sExpr (LABEL_N (N_LABEL (S nextL))) (LABEL_N (N_LABEL nextL))) (S (S nextL)) with
  66     [ pair resNextL resProg ⇒
  67      ASTFE_TO_LINEARFE_STM_RECORD_MULTI fe resNextL (JUMPBLOCK_COND fe sExpr (LABEL_N (N_LABEL (S nextL))) (LABEL_N (N_LABEL nextL))) resProg ]
  68
  69   | ASTFE_STM_IF sNelExprBody sOptBody ⇒
  70    let rec aux (pNelExprBody:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)))
  71                (pBeginL:nat) (pNextL:nat) on pNelExprBody
  72                : astfe_to_linearfe_stm_record_aux fe ≝
  73     match pNelExprBody with
  74      [ ne_nil h ⇒
  75       match sOptBody with
  76        [ None ⇒
  77         match astfe_to_linearfe_body fe (snd ?? h) pNextL (JUMPBLOCK_ABS fe (LABEL_N (N_LABEL nextL))) (S pNextL) with
  78          [ pair resNextL resProg ⇒
  79           ASTFE_TO_LINEARFE_STM_RECORD_AUX fe resNextL
  80                                            (cons ? (LINEARFE_ELEM fe (N_LABEL pBeginL) [] (JUMPBLOCK_COND fe (fst ?? h) (LABEL_N (N_LABEL pNextL)) (LABEL_N (N_LABEL nextL)))) (resProg))
  81                                            (append_to_definedAstfetolinearfe ???) ]
  82
  83        | Some optBody ⇒
  84         match astfe_to_linearfe_body fe (snd ?? h) pNextL (JUMPBLOCK_ABS fe (LABEL_N (N_LABEL nextL))) (S (S pNextL)) with
  85          [ pair resNextL resProg ⇒
  86           match astfe_to_linearfe_body fe optBody (S pNextL) (JUMPBLOCK_ABS fe (LABEL_N (N_LABEL nextL))) resNextL with
  87            [ pair resNextL' resProg' ⇒
  88             ASTFE_TO_LINEARFE_STM_RECORD_AUX fe resNextL'
  89                                              (cons ? (LINEARFE_ELEM fe (N_LABEL pBeginL) [] (JUMPBLOCK_COND fe (fst ?? h) (LABEL_N (N_LABEL pNextL)) (LABEL_N (N_LABEL (S pNextL))))) (resProg@resProg'))
  90                                              (append_to_definedAstfetolinearfe ???) ]]
  91
  92        ]
  93
  94      | ne_cons h t ⇒
  95       match astfe_to_linearfe_body fe (snd ?? h) pNextL (JUMPBLOCK_ABS fe (LABEL_N (N_LABEL nextL))) (S (S pNextL)) with
  96        [ pair resNextL resProg ⇒
  97         match aux t (S pNextL) resNextL with
  98          [ ASTFE_TO_LINEARFE_STM_RECORD_AUX resNextL' resProg' _ ⇒
  99           ASTFE_TO_LINEARFE_STM_RECORD_AUX fe resNextL'
 100                                            (cons ? (LINEARFE_ELEM fe (N_LABEL pBeginL) [] (JUMPBLOCK_COND fe (fst ?? h) (LABEL_N (N_LABEL pNextL)) (LABEL_N (N_LABEL (S pNextL))))) (resProg@resProg'))
 101                                            (append_to_definedAstfetolinearfe ???) ]]
 102
 103      ] in
 104     match aux sNelExprBody O (S nextL) with
 105      [ ASTFE_TO_LINEARFE_STM_RECORD_AUX resNextL resProg resDefined ⇒
 106       match resProg
 107        return λX:linearfe_prog fe.defined_astfetolinearfe fe X → astfe_to_linearfe_stm_record fe
 108       with
 109        (* caso dummy: impossibile! *)
 110        [ nil ⇒ λp:(defined_astfetolinearfe fe (nil ?)).False_rect ? p
 111
 112        | cons h t ⇒ λp:(defined_astfetolinearfe fe (cons ? h t)).
 113         match h with
 114          [ LINEARFE_ELEM _ _ resJump ⇒
 115           ASTFE_TO_LINEARFE_STM_RECORD_MULTI fe resNextL resJump t ]
 116
 117        ] resDefined
 118      ]
 119   ]
 120 (*
 121   ASTFE_BODY: list (astfe_stm e) → astfe_body e
 122 *)
 123 and astfe_to_linearfe_body fe (ast:astfe_body fe)
 124                               (beginL:nat) (endJump:jumpBlock fe) (nextL:nat) on ast
 125                               : Prod nat (linearfe_prog fe) ≝
 126  match ast with
 127   [ ASTFE_BODY sLStm ⇒
 128    let rec aux (pLStm:list (astfe_stm fe)) (pRes:list (linearfe_stm fe))
 129                (pBeginL:nat) (pEndJump:jumpBlock fe) (pNextL:nat)
 130                on pLStm : Prod nat (linearfe_prog fe) ≝
 131     match pLStm with
 132      [ nil ⇒
 133       pair ?? pNextL [ LINEARFE_ELEM fe (N_LABEL pBeginL) pRes pEndJump ]
 134
 135      | cons h t ⇒
 136       match astfe_to_linearfe_stm fe h pNextL with
 137        [ ASTFE_TO_LINEARFE_STM_RECORD_SINGLE resStm ⇒
 138         aux t (pRes@[ resStm ]) pBeginL pEndJump pNextL
 139        | ASTFE_TO_LINEARFE_STM_RECORD_MULTI resNextL resEndJump resProg ⇒
 140         match aux t [] pNextL pEndJump resNextL with
 141          [ pair resNextL' resProg' ⇒
 142           pair ?? resNextL' ([ LINEARFE_ELEM fe (N_LABEL pBeginL) pRes resEndJump ] @ resProg @ resProg') ]]
 143
 144      ] in aux sLStm [] beginL endJump nextL
 145   ].
 146
 147 (*
 148   ASTFE_ROOT: astfe_body e → astfe_root e
 149 *)
 150 definition astfe_to_linearfe ≝
 151 λfe.λast:astfe_root fe.match ast with
 152  [ ASTFE_ROOT body ⇒ astfe_to_linearfe_body fe body O (JUMPBLOCK_ABS fe LABEL_END) 1 ].
 153
 154 (* ***** OTTIMIZZAZIONE ***** *)
 155
 156 (* individuare gli elementi "x : [] : ABS ..." *)
 157 let rec get_useless_linearfeElem fe (prog:linearfe_prog fe) (res:list (Prod nat nat)) on prog ≝
 158  match prog with
 159   [ nil ⇒ res
 160   | cons h t ⇒ get_useless_linearfeElem fe t (res@(match h with
 161    [ LINEARFE_ELEM lbl lStm jmpB ⇒ match lStm with
 162     [ nil ⇒ match jmpB with
 163      [ JUMPBLOCK_ABS jlbl ⇒ match lbl with
 164       [ N_LABEL n ⇒ match jlbl with
 165        [ LABEL_N jlbl' ⇒ match jlbl' with
 166         [ N_LABEL n' ⇒ [ pair ?? n n' ] ]
 167        | LABEL_END ⇒ []
 168        ]]
 169      | JUMPBLOCK_COND _ _ _ ⇒ [] ]
 170     | cons _ _ ⇒  [] ]]))
 171   ].
 172
 173 (* applicare una singola trasformazione *)
 174 let rec useless_linearfeElem_trsf (ul:list (Prod nat nat)) (trsf:Prod nat nat) on ul ≝
 175  match ul with
 176   [ nil ⇒ []
 177   | cons h t ⇒ (match eqb (snd ?? h) (fst ?? trsf) with [ true ⇒ pair ?? (fst ?? h) (snd ?? trsf) | false ⇒ h ]
 178                )::(useless_linearfeElem_trsf t trsf)
 179   ].
 180
 181 (* applicare una passata completa di chiusura *)
 182 let rec useless_linearfeElem_closure_aux (preUl,ul:list (Prod nat nat)) on ul ≝
 183  match ul with
 184   [ nil ⇒ preUl
 185   | cons h t ⇒ useless_linearfeElem_closure_aux ((useless_linearfeElem_trsf preUl h)@[h]) t
 186   ].
 187
 188 definition useless_linearfeElem_closure ≝
 189 λul:list (Prod nat nat).
 190  reverse_list ? (useless_linearfeElem_closure_aux [] (reverse_list ? (useless_linearfeElem_closure_aux [] ul))).
 191
 192 inductive useless_linearfeElem_res : Type ≝
 193   USELESS_LINEARFEELEM_RES_DISCARD: nat → useless_linearfeElem_res
 194 | USELESS_LINEARFEELEM_RES_DIFF: nat → useless_linearfeElem_res.
 195
 196 (* interrogazione della mappa di trasformazione sottoposta a chiusura *)
 197 let rec useless_linearfeElem_elim (ul:list (Prod nat nat)) (n:nat) (acc:nat) on ul ≝
 198  match ul with
 199   [ nil ⇒ USELESS_LINEARFEELEM_RES_DIFF acc
 200   | cons h t ⇒ match eqb n (fst ?? h) with
 201    [ true ⇒ USELESS_LINEARFEELEM_RES_DISCARD (snd ?? h)
 202    | false ⇒ useless_linearfeElem_elim t n (match gtb n (fst ?? h) with [ true ⇒ S acc | false ⇒ acc])
 203    ]
 204   ].
 205
 206 (* eliminazione delle triple useless e compattazione delle label *)
 207 definition useless_linearfeProg_elim_aux ≝
 208 λjmpL:jumpLabel.λul:list (Prod nat nat).
 209  match jmpL with
 210   [ LABEL_N lbl ⇒ match lbl with
 211    [ N_LABEL n ⇒ match useless_linearfeElem_elim ul n O with
 212     [ USELESS_LINEARFEELEM_RES_DISCARD new ⇒ LABEL_N (N_LABEL new)
 213     | USELESS_LINEARFEELEM_RES_DIFF diff ⇒ LABEL_N (N_LABEL (n-diff))
 214     ]]
 215   | LABEL_END ⇒ LABEL_END
 216   ].
 217
 218 definition eqLabel ≝
 219 λl1,l2.match l1 with
 220  [ LABEL_N lbl1 ⇒ match l2 with
 221   [ LABEL_N lbl2 ⇒ match lbl1 with
 222    [ N_LABEL n1 ⇒ match lbl2 with
 223     [ N_LABEL n2 ⇒ eqb n1 n2 ]]
 224   | LABEL_END ⇒ false ]
 225  | LABEL_END ⇒ match l2 with
 226   [ LABEL_N _ ⇒ false | LABEL_END ⇒ true ]
 227  ].
 228
 229 lemma eq_to_eqlabel : ∀l1,l2.l1 = l2 → eqLabel l1 l2 = true.
 230  intros 2;
 231  elim l1 0;
 232  elim l2 0;
 233  [ intros;
 234    destruct H;
 235    elim j;
 236    simplify;
 237    rewrite > eq_to_eqb_true;
 238    reflexivity
 239  | intros;
 240    destruct H
 241  | intros;
 242    destruct H
 243  | intros;
 244    simplify;
 245    reflexivity
 246  ].
 247 qed.
 248
 249 lemma eqlabel_to_eq : ∀l1,l2.eqLabel l1 l2 = true → l1 = l2.
 250  intros 2;
 251  elim l1 0;
 252  elim l2 0;
 253  [ intros 2;
 254    elim j 0;
 255    elim j1 0;
 256    intros;
 257    simplify in H:(%);
 258    rewrite > (eqb_true_to_eq ?? H);
 259    reflexivity
 260  | intros;
 261    simplify in H:(%);
 262    destruct H
 263  | intros;
 264    simplify in H:(%);
 265    destruct H
 266  | intros;
 267    reflexivity
 268  ].
 269 qed.
 270
 271 let rec useless_linearfeProg_elim fe (prog:linearfe_prog fe) (ul:list (Prod nat nat)) on prog ≝
 272  match prog with
 273   [ nil ⇒ []
 274   | cons h t ⇒ match h with
 275    [ LINEARFE_ELEM lbl lStm jmpB ⇒ match lbl with
 276     [ N_LABEL n ⇒ match useless_linearfeElem_elim ul n O with
 277      (* intero elemento ridondante *)
 278      [ USELESS_LINEARFEELEM_RES_DISCARD _ ⇒ []
 279      (* la label e il salto possono necessitare di compattazione *)
 280      | USELESS_LINEARFEELEM_RES_DIFF diff ⇒
 281       [ LINEARFE_ELEM fe (N_LABEL (n-diff)) lStm (match jmpB with
 282        [ JUMPBLOCK_ABS jlbl ⇒ JUMPBLOCK_ABS fe (useless_linearfeProg_elim_aux jlbl ul)
 283        | JUMPBLOCK_COND expr jlbl1 jlbl2 ⇒
 284         (* NB: il linguaggio non ha effetti collaterali quindi COND expr x x diventa ABS x *)
 285         let jlbl1' ≝ useless_linearfeProg_elim_aux jlbl1 ul in
 286         let jlbl2' ≝ useless_linearfeProg_elim_aux jlbl2 ul in
 287         match eqLabel jlbl1' jlbl2' with
 288          [ true ⇒ JUMPBLOCK_ABS fe jlbl1'
 289          | false ⇒ JUMPBLOCK_COND fe expr jlbl1' jlbl2'
 290          ]
 291        ]
 292       )]]]]@(useless_linearfeProg_elim fe t ul)
 293   ].
 294
 295 definition useless_linearfeProg ≝
 296 λfe.λmaxProg:Prod nat (linearfe_prog fe).
 297  match maxProg with
 298   [ pair max prog ⇒
 299    let ul ≝ useless_linearfeElem_closure (get_useless_linearfeElem fe prog []) in
 300    pair ?? (max-(len_list ? ul)) (useless_linearfeProg_elim fe prog ul) ].
 301
 302 (*
 303    CONSIDERAZIONE:
 304    - il livello di annidamento medio non supera mai i 10 livelli
 305    - ogni passata puo' rimuovere un "dead" jmp COND x x
 306    - per assorbire la trasformazione serve una nuova passata
 307    - applichiamo quindi N=10 passate
 308 *)
 309 definition useless_linearfeProgMulti ≝
 310 λfe.λmaxProg:Prod nat (linearfe_prog fe).
 311  let rec aux pMaxProg n on n ≝
 312   match n with
 313    [ O ⇒ pMaxProg
 314    | S n' ⇒ aux (useless_linearfeProg fe pMaxProg) n'
 315    ] in aux maxProg 10.
 316
 317 (* ************* TEST ************* *)
 318
 319 (*
 320 definition tfe ≝
 321  snd ?? (build_trasfEnv_mapFe O [ tripleT ??? [ ch_A ] false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) ]
 322                               (pair ?? empty_map empty_flatEnv)).
 323
 324 lemma tid : astfe_id tfe false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
 325  lapply (ASTFE_ID tfe (STR_ID [ ch_A ] O));
 326  [ apply Hletin | apply I ].
 327 qed.
 328
 329 definition texp ≝
 330 λval.
 331  ASTFE_EXPR_ADD tfe AST_BASE_TYPE_BYTE8
 332                 (ASTFE_EXPR_ID tfe false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 333                                (ASTFE_VAR_ID tfe false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) tid))
 334                 (ASTFE_EXPR_BYTE8 tfe val).
 335
 336 definition tasg ≝
 337 λval.
 338  ASTFE_STM_ASG tfe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 339                    (ASTFE_VAR_ID tfe false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) tid)
 340                    (texp val).
 341
 342 definition lasg ≝
 343 λval.
 344  LINEARFE_STM_ASG tfe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 345                   (ASTFE_VAR_ID tfe false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) tid)
 346                   (texp val).
 347
 348 definition tbexp ≝
 349 λval.
 350  ASTFE_BASE_EXPR tfe AST_BASE_TYPE_BYTE8
 351                      (ASTFE_EXPR_GT tfe AST_BASE_TYPE_BYTE8
 352                                     (ASTFE_EXPR_ID tfe false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 353                                                    (ASTFE_VAR_ID tfe false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) tid))
 354                                     (ASTFE_EXPR_BYTE8 tfe val)).
 355 *)
 356
 357 (* senza (SX) e con (DX) ottimizzazione: da 0-24,25new a 0-15,16new
 358   lasg 0; lasg 1;
 359   if(tbexp 0)
 360     {
 361     while(tbexp 1)
 362       { if(tbexp 2) { lasg 2; } }
 363     lasg 3;
 364     }
 365    O : [ lasg 0 ; lasg 1 ] : COND (tbexp 0) 2 3 ;   *  O : [ lasg 0 ; lasg 1 ] : COND (tbexp 0) 2 3 ;
 366    2 : []                  : COND (tbexp 1) 5 4 ;   *  2 : []                  : COND (tbexp 1) 5 4 ;
 367    5 : []                  : COND (tbexp 2) 7 6 ;   *  5 : []                  : COND (tbexp 2) 7 6 ;
 368    7 : [ lasg 2 ]          : ABS 6 ;                *  7 : [ lasg 2 ]          : ABS 6 ;
 369    6 : []                  : COND (tbexp 1) 5 4 ;   *  6 : []                  : COND (tbexp 1) 5 4 ;
 370    4 : [ lasg 3 ]          : ABS 1 ;                *  4 : [ lasg 3 ]          : ABS 1 ;
 371
 372   else if(tbexp 3)
 373     {
 374     if(tbexp 4) {}
 375     else if(tbexp 5) {}
 376     }
 377    3 : []                  : COND (tbexp 3) 8 9 ;   *  3 : []                  : COND (tbexp 3) 1 8 ;
 378    8 : []                  : COND (tbexp 4) 11 12 ; *
 379   11 : []                  : ABS 10 ;               *
 380   12 : []                  : COND (tbexp 5) 13 10 ; *
 381   13 : []                  : ABS 10 ;               *
 382   10 : []                  : ABS 1 ;                *
 383
 384   else if(tbexp 6)
 385     {
 386     lasg 4;
 387     lasg 5;
 388     if(tbexp 7)
 389       {
 390       if(tbexp 8) { lasg 6; }
 391       lasg 7;
 392       }
 393     lasg 8;
 394     }
 395    9 : []                  : COND (tbexp 6) 14 15 ; *  8 : []                  : COND (tbexp 6) 9 10 ;
 396   14 : [ lasg 4 ; lasg 5 ] : COND (tbexp 7) 17 16 ; *  9 : [ lasg 4 ; lasg 5 ] : COND (tbexp 7) 12 11 ;
 397   17 : []                  : COND (tbexp 8) 19 18 ; * 12 : []                  : COND (tbexp 8) 14 13 ;
 398   19 : [ lasg 6 ]          : ABS 18 ;               * 14 : [ lasg 6 ]          : ABS 13 ;
 399   18 : [ lasg 7 ]          : ABS 16 ;               * 13 : [ lasg 7 ]          : ABS 11 ;
 400   16 : [ lasg 8 ]          : ABS 1 ;                * 11 : [ lasg 8 ]          : ABS 1 ;
 401
 402   else
 403     {
 404     if(tbexp 9) { lasg 9; }
 405     else if(tbexp A) {}
 406     }
 407   15 : []                  : COND (tbexp 9) 21 22 ; * 10 : []                  : COND (tbexp 9) 15 1 ;
 408   21 : [ lasg 9 ]          : ABS 20 ;               * 15 : [ lasg 9 ]          : ABS 1 ;
 409   22 : []                  : COND (tbexp A) 23 24 ; *
 410   23 : []                  : ABS 20 ;               *
 411   24 : []                  : ABS 20 ;               *
 412   20 : []                  : ABS 1 ;                *
 413
 414   ... fine dell'if principale ...
 415    1 : []                  : ABS LABEL_END ]        * ... l'ottimizzazione qui si ferma ...
 416 *)
 417
 418 (*
 419 definition tprog ≝
 420  ASTFE_ROOT tfe (
 421   ASTFE_BODY tfe [
 422    (tasg 〈x0,x0〉) ;
 423    (tasg 〈x0,x1〉) ;
 424    (ASTFE_STM_IF tfe («
 425     (pair ?? (tbexp 〈x0,x0〉)
 426      (ASTFE_BODY tfe [
 427       (ASTFE_STM_WHILE tfe (tbexp 〈x0,x1〉) (ASTFE_BODY tfe [
 428        (ASTFE_STM_IF tfe («£(pair ?? (tbexp 〈x0,x2〉) (ASTFE_BODY tfe [ tasg 〈x0,x2〉 ]))») (None ?)) ])) ;
 429       (tasg 〈x0,x3〉) ])) ;
 430     (pair ?? (tbexp 〈x0,x3〉) (ASTFE_BODY tfe [
 431      (ASTFE_STM_IF tfe («(pair ?? (tbexp 〈x0,x4〉) (ASTFE_BODY tfe []))£(pair ?? (tbexp 〈x0,x5〉) (ASTFE_BODY tfe []))») (None ?)) ])) £
 432     (pair ?? (tbexp 〈x0,x6〉)
 433      (ASTFE_BODY tfe [
 434       (tasg 〈x0,x4〉) ;
 435       (tasg 〈x0,x5〉) ;
 436       (ASTFE_STM_IF tfe («£(pair ?? (tbexp 〈x0,x7〉) (ASTFE_BODY tfe [
 437        (ASTFE_STM_IF tfe («£(pair ?? (tbexp 〈x0,x8〉) (ASTFE_BODY tfe [ tasg 〈x0,x6〉 ]))») (None ?)) ;
 438        (tasg 〈x0,x7〉) ]))») (None ?)) ;
 439       (tasg 〈x0,x8〉) ])) »)
 440     (Some ? (ASTFE_BODY tfe [
 441      (ASTFE_STM_IF tfe («(pair ?? (tbexp 〈x0,x9〉) (ASTFE_BODY tfe [ tasg 〈x0,x9〉 ]))£
 442       (pair ?? (tbexp 〈x0,xA〉) (ASTFE_BODY tfe []))»)
 443       (Some ? (ASTFE_BODY tfe [])))])))
 444    ]).
 445
 446 lemma pippo : ∃b.b=useless_linearfeProgMulti tfe (astfe_to_linearfe tfe tprog).
 447  unfold useless_linearfeProgMulti;
 448  simplify;
 449  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? %)))))))))));
 450  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? %))))))))));
 451  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? %)))))))));
 452  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? %))))))));
 453  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? %)))))));
 454  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? %))))));
 455  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? %)))));
 456  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? %))));
 457  normalize in ⊢ (? ? (λ_:?.? ? ? (? ? %)));
 458  normalize in ⊢ (? ? (λ_:?.? ? ? %));
 459  fold normalize tfe;
 460  fold normalize (lasg 〈x0,x0〉);
 461  fold normalize (lasg 〈x0,x1〉);
 462  fold normalize (lasg 〈x0,x2〉);
 463  fold normalize (lasg 〈x0,x3〉);
 464  fold normalize (lasg 〈x0,x4〉);
 465  fold normalize (lasg 〈x0,x5〉);
 466  fold normalize (lasg 〈x0,x6〉);
 467  fold normalize (lasg 〈x0,x7〉);
 468  fold normalize (lasg 〈x0,x8〉);
 469  fold normalize (lasg 〈x0,x9〉);
 470  fold normalize (tbexp 〈x0,x0〉);
 471  fold normalize (tbexp 〈x0,x1〉);
 472  fold normalize (tbexp 〈x0,x2〉);
 473  fold normalize (tbexp 〈x0,x3〉);
 474  fold normalize (tbexp 〈x0,x4〉);
 475  fold normalize (tbexp 〈x0,x5〉);
 476  fold normalize (tbexp 〈x0,x6〉);
 477  fold normalize (tbexp 〈x0,x7〉);
 478  fold normalize (tbexp 〈x0,x8〉);
 479  fold normalize (tbexp 〈x0,x9〉);
 480  fold normalize (tbexp 〈x0,xA〉);
 481  elim daemon.
 482 qed.
 483 *)