Click on a command or tactic to see a detailed view of its use.

Specification "trans".

Import "cps_sem_pres". [View cps_sem_pres]
Import "cc_sem_pres". [View cc_sem_pres]
Import "ch_sem_pres". [View ch_sem_pres]
Import "cgen_sem_pres". [View cgen_sem_pres]

Theorem nat_sem_pres: forall M M' N,
  {of M tnat} -> {compile M M'} -> {eval M (nat N)} ->
    {eval'' M' (nat' N)}.
intros. case H2.
  % CPS
  apply cps_nat_sem_pres to H1 H4 H3. apply cps_typ_pres_atom to H1 H4.
  % Closure conversion
  apply cc_nat_sem_pres to H9 H5 H8. apply cc_typ_pres_closed to H9 H5.
  % Code hoisting
  apply ch_nat_sem_pres to H11 H6 H10. apply ch_typ_pres_closed to H11 H6.
  % Code generation
  apply cg_nat_sem_pres to H13 H7 H12. search.