Welcome to Abella 2.0.5-dev.
Abella < Kind tm, tp, val, venv, tenv type.

Abella < Type app tm -> tm -> tm.

Abella < Type abs tm -> tm.

Abella < Type fix tm -> tm.

Abella < Type one tm.

Abella < Type shift tm -> tm.

Abella < Type arrow tp -> tp -> tp.

Abella < Type ground tp.

Abella < Type empty venv.

Abella < Type cons val -> venv -> venv.

Abella < Type tempty tenv.

Abella < Type tcons tp -> tenv -> tenv.

Abella < Type closure venv -> tm -> val.

Abella < Type clo (val -> val) -> val.

Abella < Define reval : venv -> tm -> val -> prop by 
reval (cons W K) one W;
reval K (fix (abs M)) (clo (c\closure (cons c K) (abs M)));
reval (cons W' K) (shift M) W := reval K M W;
reval K (abs M) (closure K (abs M));
reval K (app M N) W := exists M' W', reval K M (closure K (abs M')) /\ reval K N W' /\
  reval (cons W' K) M' W.

Abella < Define has : tenv -> tm -> tp -> prop by 
has (tcons A TE) one A;
has TE (fix M) A := has (tcons A TE) M A;
has (tcons A' TE) (shift M) A := has TE M A;
has TE (abs M) (arrow A1 A2) := has (tcons A1 TE) M A2;
has TE (app M N) A := exists A', has TE M (arrow A' A) /\ has TE N A'.

Abella < CoDefine hasty : val -> tp -> prop,	
hasty_env : venv -> tenv -> prop by 
hasty_env empty tempty;
hasty_env (cons W K) (tcons T TE) := hasty_env K TE /\ hasty W T;
hasty (closure K (abs F)) A := exists TE, has TE (abs F) A /\ hasty_env K TE;
hasty (clo (c\closure (cons c K) (abs M))) T := hasty (closure (cons (clo (c\closure (cons c K) (abs M))) K) (abs M)) T.

Abella < Theorem consistency : 
forall Ks M W TE T, reval Ks M W -> hasty_env Ks TE -> has TE M T ->
  hasty W T.


============================
 forall Ks M W TE T, reval Ks M W -> hasty_env Ks TE -> has TE M T ->
   hasty W T

consistency < induction on 1.

IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
============================
 forall Ks M W TE T, reval Ks M W @ -> hasty_env Ks TE -> has TE M T ->
   hasty W T

consistency < intros.

Variables: Ks M W TE T
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H1 : reval Ks M W @
H2 : hasty_env Ks TE
H3 : has TE M T
============================
 hasty W T

consistency < case H1.
Subgoal 1:

Variables: W TE T K
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env (cons W K) TE
H3 : has TE one T
============================
 hasty W T

Subgoal 2 is:
 hasty (clo (c\closure (cons c Ks) (abs M1))) T

Subgoal 3 is:
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < case H3.
Subgoal 1:

Variables: W T K TE1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env (cons W K) (tcons T TE1)
============================
 hasty W T

Subgoal 2 is:
 hasty (clo (c\closure (cons c Ks) (abs M1))) T

Subgoal 3 is:
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < case H2.
Subgoal 1:

Variables: W T K TE1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H4 : hasty_env K TE1
H5 : hasty W T
============================
 hasty W T

Subgoal 2 is:
 hasty (clo (c\closure (cons c Ks) (abs M1))) T

Subgoal 3 is:
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < search.
Subgoal 2:

Variables: Ks TE T M1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H3 : has TE (fix (abs M1)) T
============================
 hasty (clo (c\closure (cons c Ks) (abs M1))) T

Subgoal 3 is:
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < coinduction.
Subgoal 2:

Variables: Ks TE T M1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H3 : has TE (fix (abs M1)) T
CH : hasty (clo (c\closure (cons c Ks) (abs M1))) T ++
============================
 hasty (clo (c\closure (cons c Ks) (abs M1))) T ##

Subgoal 3 is:
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < case H3.
Subgoal 2:

Variables: Ks TE T M1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
CH : hasty (clo (c\closure (cons c Ks) (abs M1))) T ++
H4 : has (tcons T TE) (abs M1) T
============================
 hasty (clo (c\closure (cons c Ks) (abs M1))) T ##

Subgoal 3 is:
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < search.
Subgoal 3:

Variables: W TE T M1 K W'
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env (cons W' K) TE
H3 : has TE (shift M1) T
H4 : reval K M1 W *
============================
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < case H3.
Subgoal 3:

Variables: W T M1 K W' TE1 A'
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env (cons W' K) (tcons A' TE1)
H4 : reval K M1 W *
H5 : has TE1 M1 T
============================
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < case H2.
Subgoal 3:

Variables: W T M1 K W' TE1 A'
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H4 : reval K M1 W *
H5 : has TE1 M1 T
H6 : hasty_env K TE1
H7 : hasty W' A'
============================
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < apply IH to H4 H6 H5.
Subgoal 3:

Variables: W T M1 K W' TE1 A'
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H4 : reval K M1 W *
H5 : has TE1 M1 T
H6 : hasty_env K TE1
H7 : hasty W' A'
H8 : hasty W T
============================
 hasty W T

Subgoal 4 is:
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < search.
Subgoal 4:

Variables: Ks TE T M1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H3 : has TE (abs M1) T
============================
 hasty (closure Ks (abs M1)) T

Subgoal 5 is:
 hasty W T

consistency < case H3.
Subgoal 4:

Variables: Ks TE M1 A2 A1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : has (tcons A1 TE) M1 A2
============================
 hasty (closure Ks (abs M1)) (arrow A1 A2)

Subgoal 5 is:
 hasty W T

consistency < unfold.
Subgoal 4:

Variables: Ks TE M1 A2 A1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : has (tcons A1 TE) M1 A2
============================
 exists TE, has TE (abs M1) (arrow A1 A2) /\ hasty_env Ks TE

Subgoal 5 is:
 hasty W T

consistency < search.
Subgoal 5:

Variables: Ks W TE T M' W' N M1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H3 : has TE (app M1 N) T
H4 : reval Ks M1 (closure Ks (abs M')) *
H5 : reval Ks N W' *
H6 : reval (cons W' Ks) M' W *
============================
 hasty W T

consistency < case H3.
Subgoal 5:

Variables: Ks W TE T M' W' N M1 A'
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : reval Ks M1 (closure Ks (abs M')) *
H5 : reval Ks N W' *
H6 : reval (cons W' Ks) M' W *
H7 : has TE M1 (arrow A' T)
H8 : has TE N A'
============================
 hasty W T

consistency < apply IH to H4 H2 H7.
Subgoal 5:

Variables: Ks W TE T M' W' N M1 A'
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : reval Ks M1 (closure Ks (abs M')) *
H5 : reval Ks N W' *
H6 : reval (cons W' Ks) M' W *
H7 : has TE M1 (arrow A' T)
H8 : has TE N A'
H9 : hasty (closure Ks (abs M')) (arrow A' T)
============================
 hasty W T

consistency < apply IH to H5 H2 H8.
Subgoal 5:

Variables: Ks W TE T M' W' N M1 A'
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : reval Ks M1 (closure Ks (abs M')) *
H5 : reval Ks N W' *
H6 : reval (cons W' Ks) M' W *
H7 : has TE M1 (arrow A' T)
H8 : has TE N A'
H9 : hasty (closure Ks (abs M')) (arrow A' T)
H10 : hasty W' A'
============================
 hasty W T

consistency < case H9.
Subgoal 5:

Variables: Ks W TE T M' W' N M1 A' TE1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : reval Ks M1 (closure Ks (abs M')) *
H5 : reval Ks N W' *
H6 : reval (cons W' Ks) M' W *
H7 : has TE M1 (arrow A' T)
H8 : has TE N A'
H10 : hasty W' A'
H11 : has TE1 (abs M') (arrow A' T)
H12 : hasty_env Ks TE1
============================
 hasty W T

consistency < case H11.
Subgoal 5:

Variables: Ks W TE T M' W' N M1 A' TE1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : reval Ks M1 (closure Ks (abs M')) *
H5 : reval Ks N W' *
H6 : reval (cons W' Ks) M' W *
H7 : has TE M1 (arrow A' T)
H8 : has TE N A'
H10 : hasty W' A'
H12 : hasty_env Ks TE1
H13 : has (tcons A' TE1) M' T
============================
 hasty W T

consistency < apply IH to H6 _ H13.
Subgoal 5:

Variables: Ks W TE T M' W' N M1 A' TE1
IH : forall Ks M W TE T, reval Ks M W * -> hasty_env Ks TE -> has TE M T ->
       hasty W T
H2 : hasty_env Ks TE
H4 : reval Ks M1 (closure Ks (abs M')) *
H5 : reval Ks N W' *
H6 : reval (cons W' Ks) M' W *
H7 : has TE M1 (arrow A' T)
H8 : has TE N A'
H10 : hasty W' A'
H12 : hasty_env Ks TE1
H13 : has (tcons A' TE1) M' T
H14 : hasty W T
============================
 hasty W T

consistency < search.
Proof completed.
Abella <