Welcome to Abella 2.0.5-dev

Abella < Specification "append".
Reading specification "/home/yuting/Projects/svn_sparrow/papers/abella-polymorphism/schematic-polymorphism/ppdp18/website/code/./append" (from "/home/yuting/Projects/svn_sparrow/papers/abella-polymorphism/schematic-polymorphism/ppdp18/website/code/.")

Abella < Theorem app_det [A] : 
forall L1 L2 L3 L3', {append L1 L2 L3} -> {append L1 L2 L3'} -> L3 = L3'.

============================
 forall L1 L2 L3 L3', {append L1 L2 L3} -> {append L1 L2 L3'} -> L3 = L3'

app_det < induction on 1.

IH : forall L1 L2 L3 L3', {append L1 L2 L3}* -> {append L1 L2 L3'} -> L3 =
     L3'
============================
 forall L1 L2 L3 L3', {append L1 L2 L3}@ -> {append L1 L2 L3'} -> L3 = L3'

app_det < intros.

Variables: L1 L2 L3 L3'
IH : forall L1 L2 L3 L3', {append L1 L2 L3}* -> {append L1 L2 L3'} -> L3 =
     L3'
H1 : {append L1 L2 L3}@
H2 : {append L1 L2 L3'}
============================
 L3 = L3'

app_det < case H1.

Subgoal 1:

Variables: L3 L3'
IH : forall L1 L2 L3 L3', {append L1 L2 L3}* -> {append L1 L2 L3'} -> L3 =
     L3'
H2 : {append nil L3 L3'}
============================
 L3 = L3'

Subgoal 2 is:
 X :: L4 = L3'

app_det < case H2.

Subgoal 1:

Variables: L3'
IH : forall L1 L2 L3 L3', {append L1 L2 L3}* -> {append L1 L2 L3'} -> L3 =
     L3'
============================
 L3' = L3'

Subgoal 2 is:
 X :: L4 = L3'

app_det < search.

Subgoal 2:

Variables: L2 L3' L4 L6 X
IH : forall L1 L2 L3 L3', {append L1 L2 L3}* -> {append L1 L2 L3'} -> L3 =
     L3'
H2 : {append (X :: L6) L2 L3'}
H3 : {append L6 L2 L4}*
============================
 X :: L4 = L3'

app_det < case H2.

Subgoal 2:

Variables: L2 L4 L6 X L5
IH : forall L1 L2 L3 L3', {append L1 L2 L3}* -> {append L1 L2 L3'} -> L3 =
     L3'
H3 : {append L6 L2 L4}*
H4 : {append L6 L2 L5}
============================
 X :: L4 = X :: L5

app_det < apply IH to H3 H4.

Subgoal 2:

Variables: L2 L6 X L5
IH : forall L1 L2 L3 L3', {append L1 L2 L3}* -> {append L1 L2 L3'} -> L3 =
     L3'
H3 : {append L6 L2 L5}*
H4 : {append L6 L2 L5}
============================
 X :: L5 = X :: L5

app_det < search.
Proof completed.

Abella < Kind nat Type.

Abella < Theorem app_det_nat : 
forall L1 L2 L3 L3', {append L1 L2 L3} -> {append L1 L2 L3'} -> L3 = L3'.

============================
 forall L1 L2 L3 L3', {append L1 L2 L3} -> {append L1 L2 L3'} -> L3 = L3'

app_det_nat < intros.

Variables: L1 L2 L3 L3'
H1 : {append L1 L2 L3}
H2 : {append L1 L2 L3'}
============================
 L3 = L3'

app_det_nat < apply app_det to H1 H2.

Variables: L1 L2 L3'
H1 : {append L1 L2 L3'}
H2 : {append L1 L2 L3'}
============================
 L3' = L3'

app_det_nat < search.
Proof completed.

Abella < Theorem app_det_list [B] : 
forall L1 L2 L3 L3', {append L1 L2 L3} -> {append L1 L2 L3'} -> L3 = L3'.

============================
 forall L1 L2 L3 L3', {append L1 L2 L3} -> {append L1 L2 L3'} -> L3 = L3'

app_det_list < intros.

Variables: L1 L2 L3 L3'
H1 : {append L1 L2 L3}
H2 : {append L1 L2 L3'}
============================
 L3 = L3'

app_det_list < apply app_det to H1 H2.

Variables: L1 L2 L3'
H1 : {append L1 L2 L3'}
H2 : {append L1 L2 L3'}
============================
 L3' = L3'

app_det_list < search.
Proof completed.

Abella <