+definition tprog ≝
+ ASTFE_ROOT tfe (
+ ASTFE_BODY tfe [
+ (tasg 〈x0,x0〉) ;
+ (tasg 〈x0,x1〉) ;
+ (ASTFE_STM_IF tfe («
+ (pair ?? (tbexp 〈x0,x0〉)
+ (ASTFE_BODY tfe [
+ (ASTFE_STM_WHILE tfe (tbexp 〈x0,x1〉) (ASTFE_BODY tfe [
+ (ASTFE_STM_IF tfe («£(pair ?? (tbexp 〈x0,x2〉) (ASTFE_BODY tfe [ tasg 〈x0,x2〉 ]))») (None ?)) ])) ;
+ (tasg 〈x0,x3〉) ])) ;
+ (pair ?? (tbexp 〈x0,x3〉) (ASTFE_BODY tfe [
+ (ASTFE_STM_IF tfe («(pair ?? (tbexp 〈x0,x4〉) (ASTFE_BODY tfe []))£(pair ?? (tbexp 〈x0,x5〉) (ASTFE_BODY tfe []))») (None ?)) ])) £
+ (pair ?? (tbexp 〈x0,x6〉)
+ (ASTFE_BODY tfe [
+ (tasg 〈x0,x4〉) ;
+ (tasg 〈x0,x5〉) ;
+ (ASTFE_STM_IF tfe («£(pair ?? (tbexp 〈x0,x7〉) (ASTFE_BODY tfe [
+ (ASTFE_STM_IF tfe («£(pair ?? (tbexp 〈x0,x8〉) (ASTFE_BODY tfe [ tasg 〈x0,x6〉 ]))») (None ?)) ;
+ (tasg 〈x0,x7〉) ]))») (None ?)) ;
+ (tasg 〈x0,x8〉) ])) »)
+ (Some ? (ASTFE_BODY tfe [
+ (ASTFE_STM_IF tfe («(pair ?? (tbexp 〈x0,x9〉) (ASTFE_BODY tfe [ tasg 〈x0,x9〉 ]))£
+ (pair ?? (tbexp 〈x0,xA〉) (ASTFE_BODY tfe []))»)
+ (Some ? (ASTFE_BODY tfe [])))])))
+ ]).
+
+lemma pippo : ∃b.b=useless_linearfeProgMulti tfe (astfe_to_linearfe tfe tprog).
+ unfold useless_linearfeProgMulti;
+ simplify;
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? %)))))))))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? %))))))))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? (? ? %)))))))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? (? ? %))))))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? (? ? %)))))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? (? ? %))))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? (? ? %)))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? (? ? %))));
+ normalize in ⊢ (? ? (λ_:?.? ? ? (? ? %)));
+ normalize in ⊢ (? ? (λ_:?.? ? ? %));
+ fold normalize tfe;
+ fold normalize (lasg 〈x0,x0〉);
+ fold normalize (lasg 〈x0,x1〉);
+ fold normalize (lasg 〈x0,x2〉);
+ fold normalize (lasg 〈x0,x3〉);
+ fold normalize (lasg 〈x0,x4〉);
+ fold normalize (lasg 〈x0,x5〉);
+ fold normalize (lasg 〈x0,x6〉);
+ fold normalize (lasg 〈x0,x7〉);
+ fold normalize (lasg 〈x0,x8〉);
+ fold normalize (lasg 〈x0,x9〉);
+ fold normalize (tbexp 〈x0,x0〉);
+ fold normalize (tbexp 〈x0,x1〉);
+ fold normalize (tbexp 〈x0,x2〉);
+ fold normalize (tbexp 〈x0,x3〉);
+ fold normalize (tbexp 〈x0,x4〉);
+ fold normalize (tbexp 〈x0,x5〉);
+ fold normalize (tbexp 〈x0,x6〉);
+ fold normalize (tbexp 〈x0,x7〉);
+ fold normalize (tbexp 〈x0,x8〉);
+ fold normalize (tbexp 〈x0,x9〉);
+ fold normalize (tbexp 〈x0,xA〉);
+ elim daemon.
+qed.