Welcome to Abella 2.0.5-dev

Abella < Specification "trans".
Reading specification "/home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./trans" (from "/home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/.")

Abella < Import "cps_sem_pres".
Importing from /home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./cps_sem_pres
Warning: Definition might not be stratified
 ("equiv_cps" occurs to the left of ->)

Abella < Import "cc_sem_pres".
Importing from /home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./cc_sem_pres
Warning: Definition might not be stratified
 ("equiv_cc" occurs to the left of ->)

Abella < Import "ch_sem_pres".
Importing from /home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./ch_sem_pres
Warning: Definition might not be stratified
 ("equiv_ch" occurs to the left of ->)
Warning: Definition might not be stratified
 ("equiv_ch" occurs to the left of ->)

Abella < Import "cgen_sem_pres".
Importing from /home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./cgen_sem_pres
Warning: Definition might not be stratified
 ("equiv" occurs to the left of ->)
Warning: Definition might not be stratified
 ("equiv" occurs to the left of ->)

Abella < Theorem nat_sem_pres : 
forall M M' N, {of M tnat} -> {compile M M'} -> {eval M (nat N)} ->
  {eval'' M' (nat' N)}.

============================
 forall M M' N, {of M tnat} -> {compile M M'} -> {eval M (nat N)} ->
   {eval'' M' (nat' N)}

nat_sem_pres < intros.

Variables: M M' N
H1 : {of M tnat}
H2 : {compile M M'}
H3 : {eval M (nat N)}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < case H2.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < apply cps_nat_sem_pres to H1 H4 H3.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
H8 : {eval M1 (nat N)}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < apply cps_typ_pres_atom to H1 H4.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
H8 : {eval M1 (nat N)}
H9 : {of M1 tnat}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < apply cc_nat_sem_pres to H9 H5 H8.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
H8 : {eval M1 (nat N)}
H9 : {of M1 tnat}
H10 : {eval' M2 (nat' N)}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < apply cc_typ_pres_closed to H9 H5.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
H8 : {eval M1 (nat N)}
H9 : {of M1 tnat}
H10 : {eval' M2 (nat' N)}
H11 : {of' M2 tnat}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < apply ch_nat_sem_pres to H11 H6 H10.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
H8 : {eval M1 (nat N)}
H9 : {of M1 tnat}
H10 : {eval' M2 (nat' N)}
H11 : {of' M2 tnat}
H12 : {eval'' (htm FE M3) (nat' N)}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < apply ch_typ_pres_closed to H11 H6.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
H8 : {eval M1 (nat N)}
H9 : {of M1 tnat}
H10 : {eval' M2 (nat' N)}
H11 : {of' M2 tnat}
H12 : {eval'' (htm FE M3) (nat' N)}
H13 : {of'' (htm FE M3) tnat}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < apply cg_nat_sem_pres to H13 H7 H12.

Variables: M M' N M3 FE M2 M1
H1 : {of M tnat}
H3 : {eval M (nat N)}
H4 : {cps' M M1}
H5 : {cc' M1 M2}
H6 : {ch M2 (htm FE M3)}
H7 : {hcgen (htm FE M3) M'}
H8 : {eval M1 (nat N)}
H9 : {of M1 tnat}
H10 : {eval' M2 (nat' N)}
H11 : {of' M2 tnat}
H12 : {eval'' (htm FE M3) (nat' N)}
H13 : {of'' (htm FE M3) tnat}
H14 : {eval'' M' (nat' N)}
============================
 {eval'' M' (nat' N)}

nat_sem_pres < search.
Proof completed.

Abella <