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 "eval".
Importing from /home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./eval

Abella < Import "subst".
Importing from /home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./subst

Abella < Define sim : ty -> nat -> tm' -> (tm' -> tm') -> state -> tm' -> prop,	
equiv : ty -> nat -> tm' -> state -> tm' -> prop by 
sim T I M K S M' := forall J V, le J I -> {nstep' J M V} -> {val' V} ->
  (exists N V' S' N', {nstep'' N' S M' S' (K V')} /\ {add J N I} /\
       equiv T N V S' V');
equiv tnat I (nat' N) S (nat' N);
equiv tunit I unit' S unit';
equiv (prod T1 T2) I (pair' V1 V2) (st N H) (loc' L) := exists V1' V2', {lookup_heap H L (pair' V1' V2')} /\
  equiv T1 I V1 (st N H) V1' /\ equiv T2 I V2 (st N H) V2' /\ {tm' V1} /\
  {tm' V2} /\ {tm' V1'} /\ {tm' V2'};
equiv (arr' T1 T2) z (abs' R) S (abs' R') := {tm' (abs' R)} /\ {tm' (abs' R')};
equiv (arr' T1 T2) (s K) (abs' R) S (abs' R') := equiv (arr' T1 T2) K (abs' R) S (abs' R') /\
  (forall V V', equiv T1 K V S V' -> sim T2 K (R V) x\x S (R' V'));
equiv (arr T1 T2) z (clos' (abs' R) VE) (st N H) (loc' L) := exists R' VE', {lookup_heap H L (pair' (abs' R') VE')} /\
  {tm' (clos' (abs' R) VE)} /\ {tm' (pair' (abs' R') VE')} /\ {val' VE} /\
  {val' VE'};
equiv (arr T1 T2) (s K) (clos' (abs' R) VE) (st N H) (loc' L) := equiv (arr T1 T2) K (clos' (abs' R) VE) (st N H) (loc' L) /\
  (exists R' VE', {lookup_heap H L (pair' (abs' R') VE')} /\
       (forall V1 V1' V2 V2', equiv T1 K V1 (st N H) V1' ->
            equiv (arr T1 T2) K V2 (st N H) V2' ->
            sim T2 K (R (pair' V2 (pair' V1 VE))) x\x (st N H)
              (R' (pair' V2' (pair' V1' VE'))))).
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 < Define cg_ctx : (list o) -> prop by 
cg_ctx nil;
nabla x, cg_ctx (pi k\cgen x k (k x) :: L) := cg_ctx L.

Abella < Define vars_of_cg_ctx : (list o) -> (list tm') -> prop by 
vars_of_cg_ctx nil nil;
nabla x, vars_of_cg_ctx (pi k\cgen x k (k x) :: L) (x :: L') := vars_of_cg_ctx L L'.

Abella < Define subst_equiv : (list o) -> nat -> (list (map tm' tm')) -> state -> (list (map tm' tm')) -> prop by 
subst_equiv nil I nil S nil;
nabla x, subst_equiv (of' x T :: L) I (map x V :: ML) S (map x V' :: ML') := equiv T I V S V' /\ subst_equiv L I ML S ML'.

Abella < Theorem cg_nat_sem_pres : 
forall M M' V, {of'' M tnat} -> {hcgen M M'} -> {eval'' M V} -> {eval'' M' V}.

============================
 forall M M' V, {of'' M tnat} -> {hcgen M M'} -> {eval'' M V} ->
   {eval'' M' V}

cg_nat_sem_pres < intros.

Variables: M M' V
H1 : {of'' M tnat}
H2 : {hcgen M M'}
H3 : {eval'' M V}
============================
 {eval'' M' V}

cg_nat_sem_pres < case H2.

Variables: V M1 FE
H1 : {of'' (htm FE M1) tnat}
H3 : {eval'' (htm FE M1) V}
============================
 {eval'' (htm FE M1) V}

cg_nat_sem_pres < search.
Proof completed.

Abella <