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

Abella < Define ctx nil nil.

Abella < Define ctx (term X :: L1) (copy X X :: L2) := ctx L1 L2.

Abella < Theorem ctx_lemma : 
forall L1 L2 T, ctx L1 L2 -> member (term T) L1 -> member (copy T T) L2.

1 subgoal(s).

  
  ============================
   forall L1 L2 T, ctx L1 L2 -> member (term T) L1 -> member (copy T T) L2

ctx_lemma < induction on 1.

1 subgoal(s).

  
  IH : forall L1 L2 T, ctx L1 L2 * -> member (term T) L1 ->
         member (copy T T) L2
  ============================
   forall L1 L2 T, ctx L1 L2 @ -> member (term T) L1 -> member (copy T T) L2

ctx_lemma < intros.

1 subgoal(s).

  Variables: L1, L2, T
  IH : forall L1 L2 T, ctx L1 L2 * -> member (term T) L1 ->
         member (copy T T) L2
  H1 : ctx L1 L2 @
  H2 : member (term T) L1
  ============================
   member (copy T T) L2

ctx_lemma < case H1.

2 subgoal(s).

  Variables: L1, L2, T
  IH : forall L1 L2 T, ctx L1 L2 * -> member (term T) L1 ->
         member (copy T T) L2
  H2 : member (term T) nil
  ============================
   member (copy T T) nil

subgoal 2 is:
 member (copy T T) (copy X X :: L4)

ctx_lemma < case H2.

1 subgoal(s).

  Variables: L1, L2, T, L4, L3, X
  IH : forall L1 L2 T, ctx L1 L2 * -> member (term T) L1 ->
         member (copy T T) L2
  H2 : member (term T) (term X :: L3)
  H3 : ctx L3 L4 *
  ============================
   member (copy T T) (copy X X :: L4)

ctx_lemma < case H2.

2 subgoal(s).

  Variables: L1, L2, T, L4, L3, X
  IH : forall L1 L2 T, ctx L1 L2 * -> member (term T) L1 ->
         member (copy T T) L2
  H3 : ctx L3 L4 *
  ============================
   member (copy X X) (copy X X :: L4)

subgoal 2 is:
 member (copy T T) (copy X X :: L4)

ctx_lemma < search.

1 subgoal(s).

  Variables: L1, L2, T, L4, L3, X
  IH : forall L1 L2 T, ctx L1 L2 * -> member (term T) L1 ->
         member (copy T T) L2
  H3 : ctx L3 L4 *
  H4 : member (term T) L3
  ============================
   member (copy T T) (copy X X :: L4)

ctx_lemma < apply IH to H3 H4.

1 subgoal(s).

  Variables: L1, L2, T, L4, L3, X
  IH : forall L1 L2 T, ctx L1 L2 * -> member (term T) L1 ->
         member (copy T T) L2
  H3 : ctx L3 L4 *
  H4 : member (term T) L3
  H5 : member (copy T T) L4
  ============================
   member (copy T T) (copy X X :: L4)

ctx_lemma < search.
Proof completed.

Abella < Theorem copy_id : 
forall L1 L2 T, ctx L1 L2 -> {L1 |- term T} -> {L2 |- copy T T}.

1 subgoal(s).

  
  ============================
   forall L1 L2 T, ctx L1 L2 -> {L1 |- term T} -> {L2 |- copy T T}

copy_id < induction on 2.

1 subgoal(s).

  
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  ============================
   forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}@ -> {L2 |- copy T T}

copy_id < intros.

1 subgoal(s).

  Variables: L1, L2, T
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H2 : {L1 |- term T}@
  ============================
   {L2 |- copy T T}

copy_id < case H2.

3 subgoal(s).

  Variables: L1, L2, T
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H3 : member (term T) L1
  ============================
   {L2 |- copy T T}

subgoal 2 is:
 {L2 |- copy (app M N) (app M N)}

subgoal 3 is:
 {L2 |- copy (abs R) (abs R)}

copy_id < apply ctx_lemma to H1 H3.

3 subgoal(s).

  Variables: L1, L2, T
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H3 : member (term T) L1
  H4 : member (copy T T) L2
  ============================
   {L2 |- copy T T}

subgoal 2 is:
 {L2 |- copy (app M N) (app M N)}

subgoal 3 is:
 {L2 |- copy (abs R) (abs R)}

copy_id < search.

2 subgoal(s).

  Variables: L1, L2, T, N, M
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H3 : {L1 |- term M}*
  H4 : {L1 |- term N}*
  ============================
   {L2 |- copy (app M N) (app M N)}

subgoal 2 is:
 {L2 |- copy (abs R) (abs R)}

copy_id < apply IH to H1 H3.

2 subgoal(s).

  Variables: L1, L2, T, N, M
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H3 : {L1 |- term M}*
  H4 : {L1 |- term N}*
  H5 : {L2 |- copy M M}
  ============================
   {L2 |- copy (app M N) (app M N)}

subgoal 2 is:
 {L2 |- copy (abs R) (abs R)}

copy_id < apply IH to H1 H4.

2 subgoal(s).

  Variables: L1, L2, T, N, M
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H3 : {L1 |- term M}*
  H4 : {L1 |- term N}*
  H5 : {L2 |- copy M M}
  H6 : {L2 |- copy N N}
  ============================
   {L2 |- copy (app M N) (app M N)}

subgoal 2 is:
 {L2 |- copy (abs R) (abs R)}

copy_id < search.

1 subgoal(s).

  Variables: L1, L2, T, R
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H3 : {L1, term n1 |- term (R n1)}*
  ============================
   {L2 |- copy (abs R) (abs R)}

copy_id < apply IH to _ H3.

1 subgoal(s).

  Variables: L1, L2, T, R
  IH : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T}* -> {L2 |- copy T T}
  H1 : ctx L1 L2
  H3 : {L1, term n1 |- term (R n1)}*
  H4 : {L2, copy n1 n1 |- copy (R n1) (R n1)}
  ============================
   {L2 |- copy (abs R) (abs R)}

copy_id < search.
Proof completed.

Abella < Define ctx2 nil.

Abella < Define ctx2 (copy X X :: L) := ctx2 L.

Abella < Theorem ctx2_eq : 
forall L T S, ctx2 L -> member (copy T S) L -> T = S.

1 subgoal(s).

  
  ============================
   forall L T S, ctx2 L -> member (copy T S) L -> T = S

ctx2_eq < induction on 1.

1 subgoal(s).

  
  IH : forall L T S, ctx2 L * -> member (copy T S) L -> T = S
  ============================
   forall L T S, ctx2 L @ -> member (copy T S) L -> T = S

ctx2_eq < intros.

1 subgoal(s).

  Variables: L, T, S
  IH : forall L T S, ctx2 L * -> member (copy T S) L -> T = S
  H1 : ctx2 L @
  H2 : member (copy T S) L
  ============================
   T = S

ctx2_eq < case H1.

2 subgoal(s).

  Variables: L, T, S
  IH : forall L T S, ctx2 L * -> member (copy T S) L -> T = S
  H2 : member (copy T S) nil
  ============================
   T = S

subgoal 2 is:
 T = S

ctx2_eq < case H2.

1 subgoal(s).

  Variables: L, T, S, L1, X
  IH : forall L T S, ctx2 L * -> member (copy T S) L -> T = S
  H2 : member (copy T S) (copy X X :: L1)
  H3 : ctx2 L1 *
  ============================
   T = S

ctx2_eq < case H2.

2 subgoal(s).

  Variables: L, T, S, L1, X
  IH : forall L T S, ctx2 L * -> member (copy T S) L -> T = S
  H3 : ctx2 L1 *
  ============================
   X = X

subgoal 2 is:
 T = S

ctx2_eq < search.

1 subgoal(s).

  Variables: L, T, S, L1, X
  IH : forall L T S, ctx2 L * -> member (copy T S) L -> T = S
  H3 : ctx2 L1 *
  H4 : member (copy T S) L1
  ============================
   T = S

ctx2_eq < apply IH to H3 H4.

1 subgoal(s).

  Variables: L, T, S, L1, X
  IH : forall L T S, ctx2 L * -> member (copy T S) L -> T = S
  H3 : ctx2 L1 *
  H4 : member (copy S S) L1
  ============================
   S = S

ctx2_eq < search.
Proof completed.

Abella < Theorem copy_eq : 
forall L T S, ctx2 L -> {L |- copy T S} -> T = S.

1 subgoal(s).

  
  ============================
   forall L T S, ctx2 L -> {L |- copy T S} -> T = S

copy_eq < induction on 2.

1 subgoal(s).

  
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  ============================
   forall L T S, ctx2 L -> {L |- copy T S}@ -> T = S

copy_eq < intros.

1 subgoal(s).

  Variables: L, T, S
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H2 : {L |- copy T S}@
  ============================
   T = S

copy_eq < case H2.

3 subgoal(s).

  Variables: L, T, S
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H3 : member (copy T S) L
  ============================
   T = S

subgoal 2 is:
 app N M = app P Q

subgoal 3 is:
 abs R = abs S1

copy_eq < apply ctx2_eq to H1 H3.

3 subgoal(s).

  Variables: L, T, S
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H3 : member (copy S S) L
  ============================
   S = S

subgoal 2 is:
 app N M = app P Q

subgoal 3 is:
 abs R = abs S1

copy_eq < search.

2 subgoal(s).

  Variables: L, T, S, Q, P, M, N
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H3 : {L |- copy N P}*
  H4 : {L |- copy M Q}*
  ============================
   app N M = app P Q

subgoal 2 is:
 abs R = abs S1

copy_eq < apply IH to H1 H3.

2 subgoal(s).

  Variables: L, T, S, Q, P, M, N
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H3 : {L |- copy P P}*
  H4 : {L |- copy M Q}*
  ============================
   app P M = app P Q

subgoal 2 is:
 abs R = abs S1

copy_eq < apply IH to H1 H4.

2 subgoal(s).

  Variables: L, T, S, Q, P, M, N
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H3 : {L |- copy P P}*
  H4 : {L |- copy Q Q}*
  ============================
   app P Q = app P Q

subgoal 2 is:
 abs R = abs S1

copy_eq < search.

1 subgoal(s).

  Variables: L, T, S, S1, R
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H3 : {L, copy n1 n1 |- copy (R n1) (S1 n1)}*
  ============================
   abs R = abs S1

copy_eq < apply IH to _ H3.

1 subgoal(s).

  Variables: L, T, S, S1, R
  IH : forall L T S, ctx2 L -> {L |- copy T S}* -> T = S
  H1 : ctx2 L
  H3 : {L, copy n1 n1 |- copy (S1 n1) (S1 n1)}*
  ============================
   abs (x1\S1 x1) = abs S1

copy_eq < search.
Proof completed.

Abella < Theorem subst : 
forall R T S, {term T} -> {subst R T S} -> R T = S.

1 subgoal(s).

  
  ============================
   forall R T S, {term T} -> {subst R T S} -> R T = S

subst < intros.

1 subgoal(s).

  Variables: R, T, S
  H1 : {term T}
  H2 : {subst R T S}
  ============================
   R T = S

subst < case H2.

1 subgoal(s).

  Variables: R, T, S
  H1 : {term T}
  H3 : {copy n1 T |- copy (R n1) S}
  ============================
   R T = S

subst < apply copy_id to _ H1.

1 subgoal(s).

  Variables: R, T, S
  H1 : {term T}
  H3 : {copy n1 T |- copy (R n1) S}
  H4 : {copy T T}
  ============================
   R T = S

subst < inst H3 with n1 = T.

1 subgoal(s).

  Variables: R, T, S
  H1 : {term T}
  H3 : {copy n1 T |- copy (R n1) S}
  H4 : {copy T T}
  H5 : {copy T T |- copy (R T) S}
  ============================
   R T = S

subst < cut H5 with H4.

1 subgoal(s).

  Variables: R, T, S
  H1 : {term T}
  H3 : {copy n1 T |- copy (R n1) S}
  H4 : {copy T T}
  H5 : {copy T T |- copy (R T) S}
  H6 : {copy (R T) S}
  ============================
   R T = S

subst < apply copy_eq to _ H6.

1 subgoal(s).

  Variables: R, T, S
  H1 : {term T}
  H3 : {copy n1 T |- copy (R n1) (R T)}
  H4 : {copy T T}
  H5 : {copy T T |- copy (R T) (R T)}
  H6 : {copy (R T) (R T)}
  ============================
   R T = R T

subst < search.
Proof completed.

Abella < Goodbye.