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

Abella < Define nabla x, name x.

Abella < Define ctxs nil nil.

Abella < Define nabla x, ctxs (term x :: L) (neutral x :: K) := ctxs L K.

Abella < Theorem ctxs_member_term : 
forall X L K, ctxs L K -> member (term X) L -> member (neutral X) K.

1 subgoal(s).

  
  ============================
   forall X L K, ctxs L K -> member (term X) L -> member (neutral X) K

ctxs_member_term < induction on 1.

1 subgoal(s).

  
  IH : forall X L K, ctxs L K * -> member (term X) L -> member (neutral X) K
  ============================
   forall X L K, ctxs L K @ -> member (term X) L -> member (neutral X) K

ctxs_member_term < intros.

1 subgoal(s).

  Variables: X, L, K
  IH : forall X L K, ctxs L K * -> member (term X) L -> member (neutral X) K
  H1 : ctxs L K @
  H2 : member (term X) L
  ============================
   member (neutral X) K

ctxs_member_term < case H1.

2 subgoal(s).

  Variables: X, L, K
  IH : forall X L K, ctxs L K * -> member (term X) L -> member (neutral X) K
  H2 : member (term X) nil
  ============================
   member (neutral X) nil

subgoal 2 is:
 member (neutral (X n1)) (neutral n1 :: K1)

ctxs_member_term < case H2.

1 subgoal(s).

  Variables: X, L, K, K1, L1
  IH : forall X L K, ctxs L K * -> member (term X) L -> member (neutral X) K
  H2 : member (term (X n1)) (term n1 :: L1)
  H3 : ctxs L1 K1 *
  ============================
   member (neutral (X n1)) (neutral n1 :: K1)

ctxs_member_term < case H2.

2 subgoal(s).

  Variables: X, L, K, K1, L1
  IH : forall X L K, ctxs L K * -> member (term X) L -> member (neutral X) K
  H3 : ctxs L1 K1 *
  ============================
   member (neutral n1) (neutral n1 :: K1)

subgoal 2 is:
 member (neutral (X n1)) (neutral n1 :: K1)

ctxs_member_term < search.

1 subgoal(s).

  Variables: X, L, K, K1, L1
  IH : forall X L K, ctxs L K * -> member (term X) L -> member (neutral X) K
  H3 : ctxs L1 K1 *
  H4 : member (term (X n1)) L1
  ============================
   member (neutral (X n1)) (neutral n1 :: K1)

ctxs_member_term < apply IH to H3 H4.

1 subgoal(s).

  Variables: X, L, K, K1, L1
  IH : forall X L K, ctxs L K * -> member (term X) L -> member (neutral X) K
  H3 : ctxs L1 K1 *
  H4 : member (term (X n1)) L1
  H5 : member (neutral (X n1)) K1
  ============================
   member (neutral (X n1)) (neutral n1 :: K1)

ctxs_member_term < search.
Proof completed.

Abella < Theorem ctxs_var : 
forall E L K, ctxs L K -> member E K -> (exists X, E = neutral X /\ name X).

1 subgoal(s).

  
  ============================
   forall E L K, ctxs L K -> member E K -> (exists X, E = neutral X /\
     name X)

ctxs_var < induction on 1.

1 subgoal(s).

  
  IH : forall E L K, ctxs L K * -> member E K -> (exists X, E = neutral X /\
         name X)
  ============================
   forall E L K, ctxs L K @ -> member E K -> (exists X, E = neutral X /\
     name X)

ctxs_var < intros.

1 subgoal(s).

  Variables: E, L, K
  IH : forall E L K, ctxs L K * -> member E K -> (exists X, E = neutral X /\
         name X)
  H1 : ctxs L K @
  H2 : member E K
  ============================
   exists X, E = neutral X /\ name X

ctxs_var < case H1.

2 subgoal(s).

  Variables: E, L, K
  IH : forall E L K, ctxs L K * -> member E K -> (exists X, E = neutral X /\
         name X)
  H2 : member E nil
  ============================
   exists X, E = neutral X /\ name X

subgoal 2 is:
 exists X, E n1 = neutral X /\ name X

ctxs_var < case H2.

1 subgoal(s).

  Variables: E, L, K, K1, L1
  IH : forall E L K, ctxs L K * -> member E K -> (exists X, E = neutral X /\
         name X)
  H2 : member (E n1) (neutral n1 :: K1)
  H3 : ctxs L1 K1 *
  ============================
   exists X, E n1 = neutral X /\ name X

ctxs_var < case H2.

2 subgoal(s).

  Variables: E, L, K, K1, L1
  IH : forall E L K, ctxs L K * -> member E K -> (exists X, E = neutral X /\
         name X)
  H3 : ctxs L1 K1 *
  ============================
   exists X, neutral n1 = neutral X /\ name X

subgoal 2 is:
 exists X, E n1 = neutral X /\ name X

ctxs_var < search.

1 subgoal(s).

  Variables: E, L, K, K1, L1
  IH : forall E L K, ctxs L K * -> member E K -> (exists X, E = neutral X /\
         name X)
  H3 : ctxs L1 K1 *
  H4 : member (E n1) K1
  ============================
   exists X, E n1 = neutral X /\ name X

ctxs_var < apply IH to H3 H4.

1 subgoal(s).

  Variables: E, L, K, K1, L1, X
  IH : forall E L K, ctxs L K * -> member E K -> (exists X, E = neutral X /\
         name X)
  H3 : ctxs L1 K1 *
  H4 : member (neutral (X n1)) K1
  H5 : name (X n1)
  ============================
   exists X1, neutral (X n1) = neutral X1 /\ name X1

ctxs_var < search.
Proof completed.

Abella < Theorem total_ext : 
forall T L K, ctxs L K -> {L |- term T} -> {K |- normal T} \/ {non_normal T}.

1 subgoal(s).

  
  ============================
   forall T L K, ctxs L K -> {L |- term T} -> {K |- normal T} \/
     {non_normal T}

total_ext < induction on 2.

1 subgoal(s).

  
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  ============================
   forall T L K, ctxs L K -> {L |- term T}@ -> {K |- normal T} \/
     {non_normal T}

total_ext < intros.

1 subgoal(s).

  Variables: T, L, K
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H2 : {L |- term T}@
  ============================
   {K |- normal T} \/ {non_normal T}

total_ext < case H2.

3 subgoal(s).

  Variables: T, L, K
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : member (term T) L
  ============================
   {K |- normal T} \/ {non_normal T}

subgoal 2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 3 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < apply ctxs_member_term to H1 H3.

3 subgoal(s).

  Variables: T, L, K
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : member (term T) L
  H4 : member (neutral T) K
  ============================
   {K |- normal T} \/ {non_normal T}

subgoal 2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 3 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < search.

2 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < apply IH to H1 H3.

2 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H5 : {K |- normal M} \/ {non_normal M}
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < apply IH to H1 H4.

2 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H5 : {K |- normal M} \/ {non_normal M}
  H6 : {K |- normal N} \/ {non_normal N}
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < case H5.

3 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H6 : {K |- normal N} \/ {non_normal N}
  H7 : {K |- normal M}
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 3 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < case H6.

4 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H7 : {K |- normal M}
  H8 : {K |- normal N}
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 3 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 4 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < case H7.

6 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H8 : {K |- normal N}
  H9 : member (normal M) K
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (app (abs R) N)} \/ {non_normal (app (abs R) N)}

subgoal 3 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 4 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 5 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 6 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < apply ctxs_var to H1 H9.

5 subgoal(s).

  Variables: T, L, K, N, M, R
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term (abs R)}*
  H4 : {L |- term N}*
  H8 : {K |- normal N}
  H9 : {K, neutral n1 |- normal (R n1)}
  ============================
   {K |- normal (app (abs R) N)} \/ {non_normal (app (abs R) N)}

subgoal 2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 3 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 4 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 5 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < search.

4 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H8 : {K |- normal N}
  H9 : {K |- neutral M}
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 3 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 4 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < search.

3 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H7 : {K |- normal M}
  H8 : {non_normal N}
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 3 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < search.

2 subgoal(s).

  Variables: T, L, K, N, M
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L |- term M}*
  H4 : {L |- term N}*
  H6 : {K |- normal N} \/ {non_normal N}
  H7 : {non_normal M}
  ============================
   {K |- normal (app M N)} \/ {non_normal (app M N)}

subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < search.

1 subgoal(s).

  Variables: T, L, K, R
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L, term n1 |- term (R n1)}*
  ============================
   {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < apply IH to _ H3.

1 subgoal(s).

  Variables: T, L, K, R
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L, term n1 |- term (R n1)}*
  H4 : {K, neutral n1 |- normal (R n1)} \/ {non_normal (R n1)}
  ============================
   {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < case H4.

2 subgoal(s).

  Variables: T, L, K, R
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L, term n1 |- term (R n1)}*
  H5 : {K, neutral n1 |- normal (R n1)}
  ============================
   {K |- normal (abs R)} \/ {non_normal (abs R)}

subgoal 2 is:
 {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < search.

1 subgoal(s).

  Variables: T, L, K, R
  IH : forall T L K, ctxs L K -> {L |- term T}* -> {K |- normal T} \/
         {non_normal T}
  H1 : ctxs L K
  H3 : {L, term n1 |- term (R n1)}*
  H5 : {non_normal (R n1)}
  ============================
   {K |- normal (abs R)} \/ {non_normal (abs R)}

total_ext < search.
Proof completed.

Abella < Theorem total : 
forall T, {term T} -> {normal T} \/ {non_normal T}.

1 subgoal(s).

  
  ============================
   forall T, {term T} -> {normal T} \/ {non_normal T}

total < intros.

1 subgoal(s).

  Variables: T
  H1 : {term T}
  ============================
   {normal T} \/ {non_normal T}

total < apply total_ext to _ H1.

1 subgoal(s).

  Variables: T
  H1 : {term T}
  H2 : {normal T} \/ {non_normal T}
  ============================
   {normal T} \/ {non_normal T}

total < search.
Proof completed.

Abella < Theorem neutral_abs_absurd : 
forall L K R, ctxs L K -> {K |- neutral (abs R)} -> false.

1 subgoal(s).

  
  ============================
   forall L K R, ctxs L K -> {K |- neutral (abs R)} -> false

neutral_abs_absurd < intros.

1 subgoal(s).

  Variables: L, K, R
  H1 : ctxs L K
  H2 : {K |- neutral (abs R)}
  ============================
   false

neutral_abs_absurd < case H2.

1 subgoal(s).

  Variables: L, K, R
  H1 : ctxs L K
  H3 : member (neutral (abs R)) K
  ============================
   false

neutral_abs_absurd < apply ctxs_var to H1 H3.

1 subgoal(s).

  Variables: L, K, R, X
  H1 : ctxs L K
  H3 : member (neutral (abs R)) K
  H4 : name (abs R)
  ============================
   false

neutral_abs_absurd < case H4.
Proof completed.

Abella < Theorem disjoint_ext : 
forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T} -> false.

1 subgoal(s).

  
  ============================
   forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T} -> false

disjoint_ext < induction on 3.

1 subgoal(s).

  
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  ============================
   forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}@ -> false

disjoint_ext < intros.

1 subgoal(s).

  Variables: L, K, T
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H2 : {K |- normal T}
  H3 : {non_normal T}@
  ============================
   false

disjoint_ext < case H2.

3 subgoal(s).

  Variables: L, K, T
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H3 : {non_normal T}@
  H4 : member (normal T) K
  ============================
   false

subgoal 2 is:
 false

subgoal 3 is:
 false

disjoint_ext < apply ctxs_var to H1 H4.

2 subgoal(s).

  Variables: L, K, T, R
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H3 : {non_normal (abs R)}@
  H4 : {K, neutral n1 |- normal (R n1)}
  ============================
   false

subgoal 2 is:
 false

disjoint_ext < case H3.

2 subgoal(s).

  Variables: L, K, T, R
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H4 : {K, neutral n1 |- normal (R n1)}
  H5 : {non_normal (R n1)}*
  ============================
   false

subgoal 2 is:
 false

disjoint_ext < apply IH to _ H4 H5.

1 subgoal(s).

  Variables: L, K, T
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H3 : {non_normal T}@
  H4 : {K |- neutral T}
  ============================
   false

disjoint_ext < case H4.

2 subgoal(s).

  Variables: L, K, T
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H3 : {non_normal T}@
  H5 : member (neutral T) K
  ============================
   false

subgoal 2 is:
 false

disjoint_ext < apply ctxs_var to H1 H5.

2 subgoal(s).

  Variables: L, K, T, X
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H3 : {non_normal X}@
  H5 : member (neutral X) K
  H6 : name X
  ============================
   false

subgoal 2 is:
 false

disjoint_ext < case H6.

2 subgoal(s).

  Variables: L, K, T, X
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs (L n1) (K n1)
  H3 : {non_normal n1}@
  H5 : member (neutral n1) (K n1)
  ============================
   false

subgoal 2 is:
 false

disjoint_ext < case H3.

1 subgoal(s).

  Variables: L, K, T, N, M
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H3 : {non_normal (app M N)}@
  H5 : {K |- neutral M}
  H6 : {K |- normal N}
  ============================
   false

disjoint_ext < case H3.

3 subgoal(s).

  Variables: L, K, T, N, M, R
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H5 : {K |- neutral (abs R)}
  H6 : {K |- normal N}
  ============================
   false

subgoal 2 is:
 false

subgoal 3 is:
 false

disjoint_ext < apply neutral_abs_absurd to H1 H5.

2 subgoal(s).

  Variables: L, K, T, N, M
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H5 : {K |- neutral M}
  H6 : {K |- normal N}
  H7 : {non_normal M}*
  ============================
   false

subgoal 2 is:
 false

disjoint_ext < apply IH to H1 _ H7.

1 subgoal(s).

  Variables: L, K, T, N, M
  IH : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T}* -> false
  H1 : ctxs L K
  H5 : {K |- neutral M}
  H6 : {K |- normal N}
  H7 : {non_normal N}*
  ============================
   false

disjoint_ext < apply IH to H1 H6 H7.
Proof completed.

Abella < Theorem disjoint : 
forall T, {normal T} -> {non_normal T} -> false.

1 subgoal(s).

  
  ============================
   forall T, {normal T} -> {non_normal T} -> false

disjoint < intros.

1 subgoal(s).

  Variables: T
  H1 : {normal T}
  H2 : {non_normal T}
  ============================
   false

disjoint < apply disjoint_ext to _ H1 H2.
Proof completed.

Abella < Goodbye.