Welcome to Abella 2.0.2-lf

Abella < Specification "intrinsic.elf".
Reading specification "intrinsic.elf"
sig intrinsic.
  type ty lftype.
  type i lfobj.
  type arr lfobj -> lfobj -> lfobj.
  type tm lfobj -> lftype.
  type lam lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj.
  type app lfobj -> lfobj -> lfobj -> lfobj -> lfobj.
  type eval lfobj -> lfobj -> lfobj -> lftype.
  type eval/lam lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj.
  type eval/app lfobj -> lfobj -> lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj -> lfobj -> lfobj -> lfobj.
  type step lfobj -> lfobj -> lfobj -> lftype.
  type step/reduce lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj -> lfobj.
  type step/head lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj.
  type nstep lfobj -> lfobj -> lfobj -> lftype.
  type nstep/zero lfobj -> lfobj -> lfobj.
  type nstep/succ lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj -> lfobj.
  type value lfobj -> lfobj -> lftype.
  type value/abs lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj.
end.
module intrinsic.
  (* ty:type *)
  lfisty ty.
  (* i:ty *)
  lfhas i ty.
  (* arr:ty -> ty -> ty *)
  pi lf_1\lfhas lf_1 ty => pi lf_2\lfhas lf_2 ty => lfhas (arr lf_1 lf_2) ty.
  (* tm:ty -> type *)
  pi lf_1\lfhas lf_1 ty => lfisty (tm lf_1).
  (* lam:{A:ty} {B:ty} (tm A -> tm B) -> tm (arr A B) *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi lf_1\(pi lf_2\lfhas lf_2 (tm A) => lfhas (lf_1 lf_2) (tm B)) =>
        lfhas (lam A B lf_1) (tm (arr A B)).
  (* app:{A:ty} {B:ty} tm (arr A B) -> tm A -> tm B *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi lf_1\lfhas lf_1 (tm (arr A B)) =>
        pi lf_2\lfhas lf_2 (tm A) => lfhas (app A B lf_1 lf_2) (tm B).
  (* eval:{A:ty} tm A -> tm A -> type *)
  pi A\lfhas A ty =>
    pi lf_1\lfhas lf_1 (tm A) =>
      pi lf_2\lfhas lf_2 (tm A) => lfisty (eval A lf_1 lf_2).
  (* eval/lam:{A:ty} {B:ty} {R:tm A -> tm B}
       eval (arr A B) (lam A B R) (lam A B R) *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi R\(pi lf_1\lfhas lf_1 (tm A) => lfhas (R lf_1) (tm B)) =>
        lfhas (eval/lam A B R) (eval (arr A B) (lam A B R) (lam A B R)).
  (* eval/app:{A:ty} {B:ty} {M:tm (arr A B)} {N:tm A} {R:tm A -> tm B}
       {V:tm B} eval (arr A B) M (lam A B R) -> eval B (R N) V ->
       eval B (app A B M N) V *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi M\lfhas M (tm (arr A B)) =>
        pi N\lfhas N (tm A) =>
          pi R\(pi lf_1\lfhas lf_1 (tm A) => lfhas (R lf_1) (tm B)) =>
            pi V\lfhas V (tm B) =>
              pi lf_1\lfhas lf_1 (eval (arr A B) M (lam A B R)) =>
                pi lf_2\lfhas lf_2 (eval B (R N) V) =>
                  lfhas (eval/app A B M N R V lf_1 lf_2)
                    (eval B (app A B M N) V).
  (* step:{A:ty} tm A -> tm A -> type *)
  pi A\lfhas A ty =>
    pi lf_1\lfhas lf_1 (tm A) =>
      pi lf_2\lfhas lf_2 (tm A) => lfisty (step A lf_1 lf_2).
  (* step/reduce:{A:ty} {B:ty} {R:tm A -> tm B} {N:tm A}
       step B (app A B (lam A B R) N) (R N) *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi R\(pi lf_1\lfhas lf_1 (tm A) => lfhas (R lf_1) (tm B)) =>
        pi N\lfhas N (tm A) =>
          lfhas (step/reduce A B R N) (step B (app A B (lam A B R) N) (R N)).
  (* step/head:{A:ty} {B:ty} {M1:tm (arr A B)} {M2:tm (arr A B)} {N:tm A}
       step B (app A B M1 N) (app A B M2 N) *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi M1\lfhas M1 (tm (arr A B)) =>
        pi M2\lfhas M2 (tm (arr A B)) =>
          pi N\lfhas N (tm A) =>
            lfhas (step/head A B M1 M2 N)
              (step B (app A B M1 N) (app A B M2 N)).
  (* nstep:{A:ty} tm A -> tm A -> type *)
  pi A\lfhas A ty =>
    pi lf_1\lfhas lf_1 (tm A) =>
      pi lf_2\lfhas lf_2 (tm A) => lfisty (nstep A lf_1 lf_2).
  (* nstep/zero:{A:ty} {M:tm A} nstep A M M *)
  pi A\lfhas A ty =>
    pi M\lfhas M (tm A) => lfhas (nstep/zero A M) (nstep A M M).
  (* nstep/succ:{A:ty} {M1:tm A} {M2:tm A} {N:tm A} step A M1 M2 ->
       nstep A M2 N -> nstep A M1 N *)
  pi A\lfhas A ty =>
    pi M1\lfhas M1 (tm A) =>
      pi M2\lfhas M2 (tm A) =>
        pi N\lfhas N (tm A) =>
          pi lf_1\lfhas lf_1 (step A M1 M2) =>
            pi lf_2\lfhas lf_2 (nstep A M2 N) =>
              lfhas (nstep/succ A M1 M2 N lf_1 lf_2) (nstep A M1 N).
  (* value:{A:ty} tm A -> type *)
  pi A\lfhas A ty => pi lf_1\lfhas lf_1 (tm A) => lfisty (value A lf_1).
  (* value/abs:{A:ty} {B:ty} {R:tm A -> tm B} value (arr A B) (lam A B R) *)
  pi A\lfhas A ty =>
    pi B\lfhas B ty =>
      pi R\(pi lf_1\lfhas lf_1 (tm A) => lfhas (R lf_1) (tm B)) =>
        lfhas (value/abs A B R) (value (arr A B) (lam A B R)).
end.

Abella < Define progr : lfobj -> lfobj -> prop by 
progr A M := <A:ty> /\ <M:tm A> /\ (exists P, <P:value A M>);
progr A M := <A:ty> /\ <M:tm A> /\ (exists N P, <N:tm A> /\ <P:step A M N>).

Abella < Theorem progress : 
forall A M, <A:ty> -> <M:tm A> -> progr A M.

============================
 forall A M, <A:ty> -> <M:tm A> -> progr A M

progress < induction on 2.

IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
============================
 forall A M, <A:ty> -> <M:tm A>@ -> progr A M

progress < intros.

Variables: A M
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H2 : <M:tm A>@
============================
 progr A M

progress < case H2.

Subgoal 1:

Variables: B lf_1 A1
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <arr A1 B:ty>
H3 : <A1:ty>*
H4 : <B:ty>*
H5 : <n1:tm A1 |- lf_1 n1:tm B>*
============================
 progr (arr A1 B) (lam A1 B lf_1)

Subgoal 2 is:
 progr A (app A1 A lf_1 lf_2)

progress < search.

Subgoal 2:

Variables: A A1 lf_2 lf_1
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H5 : <lf_1:tm (arr A1 A)>*
H6 : <lf_2:tm A1>*
============================
 progr A (app A1 A lf_1 lf_2)

progress < apply IH to _ H5.

Subgoal 2:

Variables: A A1 lf_2 lf_1
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H5 : <lf_1:tm (arr A1 A)>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) lf_1
============================
 progr A (app A1 A lf_1 lf_2)

progress < apply IH to _ H6.

Subgoal 2:

Variables: A A1 lf_2 lf_1
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H5 : <lf_1:tm (arr A1 A)>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) lf_1
H8 : progr A1 lf_2
============================
 progr A (app A1 A lf_1 lf_2)

progress < unfold 2.

Subgoal 2.1:

Variables: A A1 lf_2 lf_1
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H5 : <lf_1:tm (arr A1 A)>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) lf_1
H8 : progr A1 lf_2
============================
 <A:ty>

Subgoal 2.2 is:
 <app A1 A lf_1 lf_2:tm A>

Subgoal 2.3 is:
 exists N P, <N:tm A> /\ <P:step A (app A1 A lf_1 lf_2) N>

progress < search.

Subgoal 2.2:

Variables: A A1 lf_2 lf_1
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H5 : <lf_1:tm (arr A1 A)>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) lf_1
H8 : progr A1 lf_2
============================
 <app A1 A lf_1 lf_2:tm A>

Subgoal 2.3 is:
 exists N P, <N:tm A> /\ <P:step A (app A1 A lf_1 lf_2) N>

progress < search.

Subgoal 2.3:

Variables: A A1 lf_2 lf_1
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H5 : <lf_1:tm (arr A1 A)>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) lf_1
H8 : progr A1 lf_2
============================
 exists N P, <N:tm A> /\ <P:step A (app A1 A lf_1 lf_2) N>

progress < case H5.

Subgoal 2.3.1:

Variables: A A1 lf_2 lf_3
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) (lam A1 A lf_3)
H8 : progr A1 lf_2
H9 : <A1:ty>*
H10 : <A:ty>*
H11 : <n1:tm A1 |- lf_3 n1:tm A>*
============================
 exists N P, <N:tm A> /\ <P:step A (app A1 A (lam A1 A lf_3) lf_2) N>

Subgoal 2.3.2 is:
 exists N P, <N:tm A> /\
   <P:step A (app A1 A (app A2 (arr A1 A) lf_3 lf_4) lf_2) N>

progress < inst H11 with n1 = lf_2.

Subgoal 2.3.1:

Variables: A A1 lf_2 lf_3
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) (lam A1 A lf_3)
H8 : progr A1 lf_2
H9 : <A1:ty>*
H10 : <A:ty>*
H11 : <n1:tm A1 |- lf_3 n1:tm A>*
H12 : <lf_2:tm A1 |- lf_3 lf_2:tm A>*
============================
 exists N P, <N:tm A> /\ <P:step A (app A1 A (lam A1 A lf_3) lf_2) N>

Subgoal 2.3.2 is:
 exists N P, <N:tm A> /\
   <P:step A (app A1 A (app A2 (arr A1 A) lf_3 lf_4) lf_2) N>

progress < cut H12 with H6.

Subgoal 2.3.1:

Variables: A A1 lf_2 lf_3
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) (lam A1 A lf_3)
H8 : progr A1 lf_2
H9 : <A1:ty>*
H10 : <A:ty>*
H11 : <n1:tm A1 |- lf_3 n1:tm A>*
H12 : <lf_2:tm A1 |- lf_3 lf_2:tm A>*
H13 : <lf_3 lf_2:tm A>
============================
 exists N P, <N:tm A> /\ <P:step A (app A1 A (lam A1 A lf_3) lf_2) N>

Subgoal 2.3.2 is:
 exists N P, <N:tm A> /\
   <P:step A (app A1 A (app A2 (arr A1 A) lf_3 lf_4) lf_2) N>

progress < exists lf_3 lf_2.

Subgoal 2.3.1:

Variables: A A1 lf_2 lf_3
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) (lam A1 A lf_3)
H8 : progr A1 lf_2
H9 : <A1:ty>*
H10 : <A:ty>*
H11 : <n1:tm A1 |- lf_3 n1:tm A>*
H12 : <lf_2:tm A1 |- lf_3 lf_2:tm A>*
H13 : <lf_3 lf_2:tm A>
============================
 exists P, <lf_3 lf_2:tm A> /\
   <P:step A (app A1 A (lam A1 A lf_3) lf_2) (lf_3 lf_2)>

Subgoal 2.3.2 is:
 exists N P, <N:tm A> /\
   <P:step A (app A1 A (app A2 (arr A1 A) lf_3 lf_4) lf_2) N>

progress < search.

Subgoal 2.3.2:

Variables: A A1 lf_2 A2 lf_4 lf_3
IH : forall A M, <A:ty> -> <M:tm A>* -> progr A M
H1 : <A:ty>
H3 : <A1:ty>*
H4 : <A:ty>*
H6 : <lf_2:tm A1>*
H7 : progr (arr A1 A) (app A2 (arr A1 A) lf_3 lf_4)
H8 : progr A1 lf_2
H9 : <A2:ty>*
H10 : <arr A1 A:ty>*
H11 : <lf_3:tm (arr A2 (arr A1 A))>*
H12 : <lf_4:tm A2>*
============================
 exists N P, <N:tm A> /\
   <P:step A (app A1 A (app A2 (arr A1 A) lf_3 lf_4) lf_2) N>

progress < search.
Proof completed.

Abella < Goodbye.