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 <