Welcome to Abella 1.1.3-dev2 Reading clauses from nd-to-seq.mod

Abella < Define convert nil nil.

Abella < Define convert (nd G :: L) (hyp G :: K) := convert L K.

Abella < Theorem convert_member : 
forall L K H, convert L K -> member (nd H) L -> member (hyp H) K.

1 subgoal(s).

  
  ============================
   forall L K H, convert L K -> member (nd H) L -> member (hyp H) K

convert_member < induction on 2.

1 subgoal(s).

  
  IH : forall L K H, convert L K -> member (nd H) L * -> member (hyp H) K
  ============================
   forall L K H, convert L K -> member (nd H) L @ -> member (hyp H) K

convert_member < intros.

1 subgoal(s).

  Variables: L, K, H
  IH : forall L K H, convert L K -> member (nd H) L * -> member (hyp H) K
  H1 : convert L K
  H2 : member (nd H) L @
  ============================
   member (hyp H) K

convert_member < case H2.

2 subgoal(s).

  Variables: L, K, H, L1
  IH : forall L K H, convert L K -> member (nd H) L * -> member (hyp H) K
  H1 : convert (nd H :: L1) K
  ============================
   member (hyp H) K

subgoal 2 is:
 member (hyp H) K

convert_member < case H1.

2 subgoal(s).

  Variables: L, K, H, L1, K1
  IH : forall L K H, convert L K -> member (nd H) L * -> member (hyp H) K
  H3 : convert L1 K1
  ============================
   member (hyp H) (hyp H :: K1)

subgoal 2 is:
 member (hyp H) K

convert_member < search.

1 subgoal(s).

  Variables: L, K, H, L1, B
  IH : forall L K H, convert L K -> member (nd H) L * -> member (hyp H) K
  H1 : convert (B :: L1) K
  H3 : member (nd H) L1 *
  ============================
   member (hyp H) K

convert_member < case H1.

1 subgoal(s).

  Variables: L, K, H, L1, B, K1, G
  IH : forall L K H, convert L K -> member (nd H) L * -> member (hyp H) K
  H3 : member (nd H) L1 *
  H4 : convert L1 K1
  ============================
   member (hyp H) (hyp G :: K1)

convert_member < apply IH to H4 H3.

1 subgoal(s).

  Variables: L, K, H, L1, B, K1, G
  IH : forall L K H, convert L K -> member (nd H) L * -> member (hyp H) K
  H3 : member (nd H) L1 *
  H4 : convert L1 K1
  H5 : member (hyp H) K1
  ============================
   member (hyp H) (hyp G :: K1)

convert_member < search.
Proof completed.

Abella < Theorem nd_to_seq_ext : 
forall L K G, {L |- nd G} -> convert L K -> {K |- conc G}.

1 subgoal(s).

  
  ============================
   forall L K G, {L |- nd G} -> convert L K -> {K |- conc G}

nd_to_seq_ext < induction on 1.

1 subgoal(s).

  
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  ============================
   forall L K G, {L |- nd G}@ -> convert L K -> {K |- conc G}

nd_to_seq_ext < intros.

1 subgoal(s).

  Variables: L, K, G
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H1 : {L |- nd G}@
  H2 : convert L K
  ============================
   {K |- conc G}

nd_to_seq_ext < case H1.

3 subgoal(s).

  Variables: L, K, G
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H2 : convert L K
  H3 : member (nd G) L
  ============================
   {K |- conc G}

subgoal 2 is:
 {K |- conc (imp A B)}

subgoal 3 is:
 {K |- conc G}

nd_to_seq_ext < apply convert_member to H2 H3.

3 subgoal(s).

  Variables: L, K, G
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H2 : convert L K
  H3 : member (nd G) L
  H4 : member (hyp G) K
  ============================
   {K |- conc G}

subgoal 2 is:
 {K |- conc (imp A B)}

subgoal 3 is:
 {K |- conc G}

nd_to_seq_ext < search.

2 subgoal(s).

  Variables: L, K, G, B, A
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H2 : convert L K
  H3 : {L, nd A |- nd B}*
  ============================
   {K |- conc (imp A B)}

subgoal 2 is:
 {K |- conc G}

nd_to_seq_ext < apply IH to H3 _.

2 subgoal(s).

  Variables: L, K, G, B, A
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H2 : convert L K
  H3 : {L, nd A |- nd B}*
  H4 : {K, hyp A |- conc B}
  ============================
   {K |- conc (imp A B)}

subgoal 2 is:
 {K |- conc G}

nd_to_seq_ext < search.

1 subgoal(s).

  Variables: L, K, G, A
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H2 : convert L K
  H3 : {L |- nd (imp A G)}*
  H4 : {L |- nd A}*
  ============================
   {K |- conc G}

nd_to_seq_ext < apply IH to H3 H2.

1 subgoal(s).

  Variables: L, K, G, A
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H2 : convert L K
  H3 : {L |- nd (imp A G)}*
  H4 : {L |- nd A}*
  H5 : {K |- conc (imp A G)}
  ============================
   {K |- conc G}

nd_to_seq_ext < apply IH to H4 H2.

1 subgoal(s).

  Variables: L, K, G, A
  IH : forall L K G, {L |- nd G}* -> convert L K -> {K |- conc G}
  H2 : convert L K
  H3 : {L |- nd (imp A G)}*
  H4 : {L |- nd A}*
  H5 : {K |- conc (imp A G)}
  H6 : {K |- conc A}
  ============================
   {K |- conc G}

nd_to_seq_ext < search.
Proof completed.

Abella < Theorem nd_to_seq : 
forall G, {nd G} -> {conc G}.

1 subgoal(s).

  
  ============================
   forall G, {nd G} -> {conc G}

nd_to_seq < intros.

1 subgoal(s).

  Variables: G
  H1 : {nd G}
  ============================
   {conc G}

nd_to_seq < apply nd_to_seq_ext to H1 _.

1 subgoal(s).

  Variables: G
  H1 : {nd G}
  H2 : {conc G}
  ============================
   {conc G}

nd_to_seq < search.
Proof completed.

Abella < Goodbye.