Welcome to Abella 1.1.3-dev2 Reading clauses from cascade.mod

Abella < Define subst nil T T.

Abella < Define nabla x, subst (pair x K :: L) (T x) S := subst L (T K) S.

Abella < Theorem subst_app : 
forall L T R S, subst L (app T R) S -> (exists U V, S = app U V /\
  subst L T U /\ subst L R V).

1 subgoal(s).

  
  ============================
   forall L T R S, subst L (app T R) S -> (exists U V, S = app U V /\
     subst L T U /\ subst L R V)

subst_app < induction on 1.

1 subgoal(s).

  
  IH : forall L T R S, subst L (app T R) S * -> (exists U V, S = app U V /\
         subst L T U /\ subst L R V)
  ============================
   forall L T R S, subst L (app T R) S @ -> (exists U V, S = app U V /\
     subst L T U /\ subst L R V)

subst_app < intros.

1 subgoal(s).

  Variables: L, T, R, S
  IH : forall L T R S, subst L (app T R) S * -> (exists U V, S = app U V /\
         subst L T U /\ subst L R V)
  H1 : subst L (app T R) S @
  ============================
   exists U V, S = app U V /\ subst L T U /\ subst L R V

subst_app < case H1.

2 subgoal(s).

  Variables: L, T, R, S
  IH : forall L T R S, subst L (app T R) S * -> (exists U V, S = app U V /\
         subst L T U /\ subst L R V)
  ============================
   exists U V, app T R = app U V /\ subst nil T U /\ subst nil R V

subgoal 2 is:
 exists U V, S1 = app U V /\ subst (pair n1 K :: L1) (T n1) U /\
   subst (pair n1 K :: L1) (R n1) V

subst_app < search.

1 subgoal(s).

  Variables: L, T, R, S, S1, L1, K
  IH : forall L T R S, subst L (app T R) S * -> (exists U V, S = app U V /\
         subst L T U /\ subst L R V)
  H2 : subst L1 (app (T K) (R K)) S1 *
  ============================
   exists U V, S1 = app U V /\ subst (pair n1 K :: L1) (T n1) U /\
     subst (pair n1 K :: L1) (R n1) V

subst_app < apply IH to H2.

1 subgoal(s).

  Variables: L, T, R, S, S1, L1, K, U, V
  IH : forall L T R S, subst L (app T R) S * -> (exists U V, S = app U V /\
         subst L T U /\ subst L R V)
  H2 : subst L1 (app (T K) (R K)) (app U V) *
  H3 : subst L1 (T K) U
  H4 : subst L1 (R K) V
  ============================
   exists U1 V1, app U V = app U1 V1 /\ subst (pair n1 K :: L1) (T n1) U1 /\
     subst (pair n1 K :: L1) (R n1) V1

subst_app < search.
Proof completed.

Abella < Theorem subst_abs : 
forall L T R, subst L (abs T) R -> (exists S, R = abs S /\ (nabla z,
  subst L (T z) (S z))).

1 subgoal(s).

  
  ============================
   forall L T R, subst L (abs T) R -> (exists S, R = abs S /\ (nabla z,
     subst L (T z) (S z)))

subst_abs < induction on 1.

1 subgoal(s).

  
  IH : forall L T R, subst L (abs T) R * -> (exists S, R = abs S /\ (nabla z,
         subst L (T z) (S z)))
  ============================
   forall L T R, subst L (abs T) R @ -> (exists S, R = abs S /\ (nabla z,
     subst L (T z) (S z)))

subst_abs < intros.

1 subgoal(s).

  Variables: L, T, R
  IH : forall L T R, subst L (abs T) R * -> (exists S, R = abs S /\ (nabla z,
         subst L (T z) (S z)))
  H1 : subst L (abs T) R @
  ============================
   exists S, R = abs S /\ (nabla z, subst L (T z) (S z))

subst_abs < case H1.

2 subgoal(s).

  Variables: L, T, R
  IH : forall L T R, subst L (abs T) R * -> (exists S, R = abs S /\ (nabla z,
         subst L (T z) (S z)))
  ============================
   exists S, abs T = abs S /\ (nabla z, subst nil (T z) (S z))

subgoal 2 is:
 exists S1, S = abs S1 /\ (nabla z, subst (pair n1 K :: L1) (T n1 z) (S1 z))

subst_abs < search.

1 subgoal(s).

  Variables: L, T, R, S, L1, K
  IH : forall L T R, subst L (abs T) R * -> (exists S, R = abs S /\ (nabla z,
         subst L (T z) (S z)))
  H2 : subst L1 (abs (T K)) S *
  ============================
   exists S1, S = abs S1 /\ (nabla z,
     subst (pair n1 K :: L1) (T n1 z) (S1 z))

subst_abs < apply IH to H2.

1 subgoal(s).

  Variables: L, T, R, S, L1, K, S1
  IH : forall L T R, subst L (abs T) R * -> (exists S, R = abs S /\ (nabla z,
         subst L (T z) (S z)))
  H2 : subst L1 (abs (T K)) (abs S1) *
  H3 : subst L1 (T K n1) (S1 n1)
  ============================
   exists S2, abs S1 = abs S2 /\ (nabla z,
     subst (pair n1 K :: L1) (T n1 z) (S2 z))

subst_abs < search.
Proof completed.

Abella < Goodbye.