Welcome to Abella 2.0.4-dev
```Abella < Specification "higher-order".

```
```Abella < Theorem split :
forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K} ->
(exists J, {mappred R L J} /\ {mappred S J K}).

```
```
============================
forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K} ->
(exists J, {mappred R L J} /\ {mappred S J K})

split < induction on 1.
```
```
IH : forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}* ->
(exists J, {mappred R L J} /\ {mappred S J K})
============================
forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}@ ->
(exists J, {mappred R L J} /\ {mappred S J K})

split < intros.
```
```
Variables: R S L K
IH : forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}* ->
(exists J, {mappred R L J} /\ {mappred S J K})
H1 : {mappred (x\y\exist (z\and (R x z) (S z y))) L K}@
============================
exists J, {mappred R L J} /\ {mappred S J K}

split < case H1.
```
```Subgoal 1:

Variables: R S
IH : forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}* ->
(exists J, {mappred R L J} /\ {mappred S J K})
============================
exists J, {mappred R anil J} /\ {mappred S J anil}

Subgoal 2 is:
exists J, {mappred R (acons X XS) J} /\ {mappred S J (acons Y YS)}

split < search.
```
```Subgoal 2:

Variables: R S YS XS Y X
IH : forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}* ->
(exists J, {mappred R L J} /\ {mappred S J K})
H2 : {exist (z\and (R X z) (S z Y))}*
H3 : {mappred (x\y\exist (z\and (R x z) (S z y))) XS YS}*
============================
exists J, {mappred R (acons X XS) J} /\ {mappred S J (acons Y YS)}

split < case H2.
```
```Subgoal 2:

Variables: R S YS XS Y X X1
IH : forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}* ->
(exists J, {mappred R L J} /\ {mappred S J K})
H3 : {mappred (x\y\exist (z\and (R x z) (S z y))) XS YS}*
H4 : {and (R X X1) (S X1 Y)}*
============================
exists J, {mappred R (acons X XS) J} /\ {mappred S J (acons Y YS)}

split < case H4.
```
```Subgoal 2:

Variables: R S YS XS Y X X1
IH : forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}* ->
(exists J, {mappred R L J} /\ {mappred S J K})
H3 : {mappred (x\y\exist (z\and (R x z) (S z y))) XS YS}*
H5 : {R X X1}*
H6 : {S X1 Y}*
============================
exists J, {mappred R (acons X XS) J} /\ {mappred S J (acons Y YS)}

split < apply IH to H3.
```
```Subgoal 2:

Variables: R S YS XS Y X X1 J
IH : forall R S L K, {mappred (x\y\exist (z\and (R x z) (S z y))) L K}* ->
(exists J, {mappred R L J} /\ {mappred S J K})
H3 : {mappred (x\y\exist (z\and (R x z) (S z y))) XS YS}*
H5 : {R X X1}*
H6 : {S X1 Y}*
H7 : {mappred (z1\z2\R z1 z2) XS J}
H8 : {mappred (z1\z2\S z1 z2) J YS}
============================
exists J, {mappred R (acons X XS) J} /\ {mappred S J (acons Y YS)}

split < search.
Proof completed.
```
```Abella < Theorem combine :
forall R S L K J, {mappred R L J} -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}.

```
```
============================
forall R S L K J, {mappred R L J} -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}

combine < induction on 1.
```
```
IH : forall R S L K J, {mappred R L J}* -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}
============================
forall R S L K J, {mappred R L J}@ -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}

combine < intros.
```
```
Variables: R S L K J
IH : forall R S L K J, {mappred R L J}* -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}
H1 : {mappred R L J}@
H2 : {mappred S J K}
============================
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}

combine < case H1.
```
```Subgoal 1:

Variables: R S K
IH : forall R S L K J, {mappred R L J}* -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}
H2 : {mappred S anil K}
============================
{mappred (x\y\exist (z\and (R x z) (S z y))) anil K}

Subgoal 2 is:
{mappred (x\y\exist (z\and (R x z) (S z y))) (acons X XS) K}

combine < case H2.
```
```Subgoal 1:

Variables: R S
IH : forall R S L K J, {mappred R L J}* -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}
============================
{mappred (x\y\exist (z\and (R x z) (S z y))) anil anil}

Subgoal 2 is:
{mappred (x\y\exist (z\and (R x z) (S z y))) (acons X XS) K}

combine < search.
```
```Subgoal 2:

Variables: R S K YS XS Y X
IH : forall R S L K J, {mappred R L J}* -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}
H2 : {mappred S (acons Y YS) K}
H3 : {R X Y}*
H4 : {mappred R XS YS}*
============================
{mappred (x\y\exist (z\and (R x z) (S z y))) (acons X XS) K}

combine < case H2.
```
```Subgoal 2:

Variables: R S YS XS Y X YS1 Y1
IH : forall R S L K J, {mappred R L J}* -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}
H3 : {R X Y}*
H4 : {mappred R XS YS}*
H5 : {S Y Y1}
H6 : {mappred S YS YS1}
============================
{mappred (x\y\exist (z\and (R x z) (S z y))) (acons X XS) (acons Y1 YS1)}

combine < apply IH to H4 H6.
```
```Subgoal 2:

Variables: R S YS XS Y X YS1 Y1
IH : forall R S L K J, {mappred R L J}* -> {mappred S J K} ->
{mappred (x\y\exist (z\and (R x z) (S z y))) L K}
H3 : {R X Y}*
H4 : {mappred R XS YS}*
H5 : {S Y Y1}
H6 : {mappred S YS YS1}
H7 : {mappred (x\y\exist (z\and (R x z) (S z y))) XS YS1}
============================
{mappred (x\y\exist (z\and (R x z) (S z y))) (acons X XS) (acons Y1 YS1)}

combine < search.
Proof completed.
```
```Abella < Theorem deterministic :
forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1} -> {mappred R L K2} -> K1 =
K2.

```
```
============================
forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1} -> {mappred R L K2} -> K1 =
K2

deterministic < induction on 2.
```
```
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
============================
forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}@ -> {mappred R L K2} -> K1 =
K2

deterministic < intros.
```
```
Variables: R L K1 K2
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
H1 : forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2
H2 : {mappred R L K1}@
H3 : {mappred R L K2}
============================
K1 = K2

deterministic < case H2.
```
```Subgoal 1:

Variables: R K2
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
H1 : forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2
H3 : {mappred R anil K2}
============================
anil = K2

Subgoal 2 is:
acons Y YS = K2

deterministic < case H3.
```
```Subgoal 1:

Variables: R
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
H1 : forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2
============================
anil = anil

Subgoal 2 is:
acons Y YS = K2

deterministic < search.
```
```Subgoal 2:

Variables: R K2 YS XS Y X
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
H1 : forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2
H3 : {mappred R (acons X XS) K2}
H4 : {R X Y}*
H5 : {mappred R XS YS}*
============================
acons Y YS = K2

deterministic < case H3.
```
```Subgoal 2:

Variables: R YS XS Y X YS1 Y1
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
H1 : forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2
H4 : {R X Y}*
H5 : {mappred R XS YS}*
H6 : {R X Y1}
H7 : {mappred R XS YS1}
============================
acons Y YS = acons Y1 YS1

deterministic < apply H1 to H4 H6.
```
```Subgoal 2:

Variables: R YS XS X YS1 Y1
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
H1 : forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2
H4 : {R X Y1}*
H5 : {mappred R XS YS}*
H6 : {R X Y1}
H7 : {mappred R XS YS1}
============================
acons Y1 YS = acons Y1 YS1

deterministic < apply IH to H1 H5 H7.
```
```Subgoal 2:

Variables: R XS X YS1 Y1
IH : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
{mappred R L K1}* -> {mappred R L K2} -> K1 =
K2
H1 : forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2
H4 : {R X Y1}*
H5 : {mappred R XS YS1}*
H6 : {R X Y1}
H7 : {mappred R XS YS1}
============================
acons Y1 YS1 = acons Y1 YS1

deterministic < search.
Proof completed.
```
```Abella < Theorem swap1 :
forall R L K, {mappred (swap R) L K} -> {mappred R K L}.

```
```
============================
forall R L K, {mappred (swap R) L K} -> {mappred R K L}

swap1 < induction on 1.
```
```
IH : forall R L K, {mappred (swap R) L K}* -> {mappred R K L}
============================
forall R L K, {mappred (swap R) L K}@ -> {mappred R K L}

swap1 < intros.
```
```
Variables: R L K
IH : forall R L K, {mappred (swap R) L K}* -> {mappred R K L}
H1 : {mappred (swap R) L K}@
============================
{mappred R K L}

swap1 < case H1.
```
```Subgoal 1:

Variables: R
IH : forall R L K, {mappred (swap R) L K}* -> {mappred R K L}
============================
{mappred R anil anil}

Subgoal 2 is:
{mappred R (acons Y YS) (acons X XS)}

swap1 < search.
```
```Subgoal 2:

Variables: R YS XS Y X
IH : forall R L K, {mappred (swap R) L K}* -> {mappred R K L}
H2 : {swap R X Y}*
H3 : {mappred (swap R) XS YS}*
============================
{mappred R (acons Y YS) (acons X XS)}

swap1 < case H2.
```
```Subgoal 2:

Variables: R YS XS Y X
IH : forall R L K, {mappred (swap R) L K}* -> {mappred R K L}
H3 : {mappred (swap R) XS YS}*
H4 : {R Y X}*
============================
{mappred R (acons Y YS) (acons X XS)}

swap1 < apply IH to H3.
```
```Subgoal 2:

Variables: R YS XS Y X
IH : forall R L K, {mappred (swap R) L K}* -> {mappred R K L}
H3 : {mappred (swap R) XS YS}*
H4 : {R Y X}*
H5 : {mappred R YS XS}
============================
{mappred R (acons Y YS) (acons X XS)}

swap1 < search.
Proof completed.
```
```Abella < Theorem swap2 :
forall R L K, {mappred R K L} -> {mappred (swap R) L K}.

```
```
============================
forall R L K, {mappred R K L} -> {mappred (swap R) L K}

swap2 < induction on 1.
```
```
IH : forall R L K, {mappred R K L}* -> {mappred (swap R) L K}
============================
forall R L K, {mappred R K L}@ -> {mappred (swap R) L K}

swap2 < intros.
```
```
Variables: R L K
IH : forall R L K, {mappred R K L}* -> {mappred (swap R) L K}
H1 : {mappred R K L}@
============================
{mappred (swap R) L K}

swap2 < case H1.
```
```Subgoal 1:

Variables: R
IH : forall R L K, {mappred R K L}* -> {mappred (swap R) L K}
============================
{mappred (swap R) anil anil}

Subgoal 2 is:
{mappred (swap R) (acons Y YS) (acons X XS)}

swap2 < search.
```
```Subgoal 2:

Variables: R YS XS Y X
IH : forall R L K, {mappred R K L}* -> {mappred (swap R) L K}
H2 : {R X Y}*
H3 : {mappred R XS YS}*
============================
{mappred (swap R) (acons Y YS) (acons X XS)}

swap2 < apply IH to H3.
```
```Subgoal 2:

Variables: R YS XS Y X
IH : forall R L K, {mappred R K L}* -> {mappred (swap R) L K}
H2 : {R X Y}*
H3 : {mappred R XS YS}*
H4 : {mappred (swap R) YS XS}
============================
{mappred (swap R) (acons Y YS) (acons X XS)}

swap2 < search.
Proof completed.
```
```Abella < Define reflexive : (a -> a -> o) -> prop by
reflexive P := forall X, {P X X}.

```
```Abella < Define transitive : (a -> a -> o) -> prop by
transitive P := forall X Y Z, {P X Y} -> {P Y Z} -> {P X Z}.

```
```Abella < Theorem star_reflexive :
forall P, reflexive (star P).

```
```
============================
forall P, reflexive (star P)

star_reflexive < search.
Proof completed.
```
```Abella < Theorem star_transitive :
forall P, transitive (star P).

```
```
============================
forall P, transitive (star P)

star_transitive < intros.
```
```
Variables: P
============================
transitive (star P)

star_transitive < unfold.
```
```
Variables: P
============================
forall X Y Z, {star P X Y} -> {star P Y Z} -> {star P X Z}

star_transitive < induction on 1.
```
```
Variables: P
IH : forall X Y Z, {star P X Y}* -> {star P Y Z} -> {star P X Z}
============================
forall X Y Z, {star P X Y}@ -> {star P Y Z} -> {star P X Z}

star_transitive < intros.
```
```
Variables: P X Y Z
IH : forall X Y Z, {star P X Y}* -> {star P Y Z} -> {star P X Z}
H1 : {star P X Y}@
H2 : {star P Y Z}
============================
{star P X Z}

star_transitive < case H1.
```
```Subgoal 1:

Variables: P Y Z
IH : forall X Y Z, {star P X Y}* -> {star P Y Z} -> {star P X Z}
H2 : {star P Y Z}
============================
{star P Y Z}

Subgoal 2 is:
{star P X Z}

star_transitive < search.
```
```Subgoal 2:

Variables: P X Y Z Z1
IH : forall X Y Z, {star P X Y}* -> {star P Y Z} -> {star P X Z}
H2 : {star P Y Z}
H3 : {P X Z1}*
H4 : {star P Z1 Y}*
============================
{star P X Z}

star_transitive < apply IH to H4 H2.
```
```Subgoal 2:

Variables: P X Y Z Z1
IH : forall X Y Z, {star P X Y}* -> {star P Y Z} -> {star P X Z}
H2 : {star P Y Z}
H3 : {P X Z1}*
H4 : {star P Z1 Y}*
H5 : {star P Z1 Z}
============================
{star P X Z}

star_transitive < search.
Proof completed.
```
```Abella < Define contained_in : (a -> a -> o) -> (a -> a -> o) -> prop by
contained_in P S := forall X Y, {P X Y} -> {S X Y}.

```
```Abella < Theorem star_minimal :
forall P S, contained_in P S -> reflexive S -> transitive S ->
contained_in (star P) S.

```
```
============================
forall P S, contained_in P S -> reflexive S -> transitive S ->
contained_in (star P) S

star_minimal < intros.
```
```
Variables: P S
H1 : contained_in P S
H2 : reflexive S
H3 : transitive S
============================
contained_in (star P) S

star_minimal < unfold.
```
```
Variables: P S
H1 : contained_in P S
H2 : reflexive S
H3 : transitive S
============================
forall X Y, {star P X Y} -> {S X Y}

star_minimal < induction on 1.
```
```
Variables: P S
H1 : contained_in P S
H2 : reflexive S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
============================
forall X Y, {star P X Y}@ -> {S X Y}

star_minimal < intros.
```
```
Variables: P S X Y
H1 : contained_in P S
H2 : reflexive S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H4 : {star P X Y}@
============================
{S X Y}

star_minimal < case H4.
```
```Subgoal 1:

Variables: P S Y
H1 : contained_in P S
H2 : reflexive S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
============================
{S Y Y}

Subgoal 2 is:
{S X Y}

star_minimal < case H2.
```
```Subgoal 1:

Variables: P S Y
H1 : contained_in P S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H5 : forall X, {S X X}
============================
{S Y Y}

Subgoal 2 is:
{S X Y}

star_minimal < backchain H5.
```
```Subgoal 2:

Variables: P S X Y Z
H1 : contained_in P S
H2 : reflexive S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H5 : {P X Z}*
H6 : {star P Z Y}*
============================
{S X Y}

star_minimal < apply IH to H6.
```
```Subgoal 2:

Variables: P S X Y Z
H1 : contained_in P S
H2 : reflexive S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H5 : {P X Z}*
H6 : {star P Z Y}*
H7 : {S Z Y}
============================
{S X Y}

star_minimal < case H1.
```
```Subgoal 2:

Variables: P S X Y Z
H2 : reflexive S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H5 : {P X Z}*
H6 : {star P Z Y}*
H7 : {S Z Y}
H8 : forall X Y, {P X Y} -> {S X Y}
============================
{S X Y}

star_minimal < apply H8 to H5.
```
```Subgoal 2:

Variables: P S X Y Z
H2 : reflexive S
H3 : transitive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H5 : {P X Z}*
H6 : {star P Z Y}*
H7 : {S Z Y}
H8 : forall X Y, {P X Y} -> {S X Y}
H9 : {S X Z}
============================
{S X Y}

star_minimal < case H3.
```
```Subgoal 2:

Variables: P S X Y Z
H2 : reflexive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H5 : {P X Z}*
H6 : {star P Z Y}*
H7 : {S Z Y}
H8 : forall X Y, {P X Y} -> {S X Y}
H9 : {S X Z}
H10 : forall X Y Z, {S X Y} -> {S Y Z} -> {S X Z}
============================
{S X Y}

star_minimal < apply H10 to H9 H7.
```
```Subgoal 2:

Variables: P S X Y Z
H2 : reflexive S
IH : forall X Y, {star P X Y}* -> {S X Y}
H5 : {P X Z}*
H6 : {star P Z Y}*
H7 : {S Z Y}
H8 : forall X Y, {P X Y} -> {S X Y}
H9 : {S X Z}
H10 : forall X Y Z, {S X Y} -> {S Y Z} -> {S X Z}
H11 : {S X Y}
============================
{S X Y}

star_minimal < search.
Proof completed.
```
```Abella < Theorem star_vacuous :
forall P, reflexive P -> transitive P -> contained_in (star P) P.

```
```
============================
forall P, reflexive P -> transitive P -> contained_in (star P) P

star_vacuous < intros.
```
```
Variables: P
H1 : reflexive P
H2 : transitive P
============================
contained_in (star P) P

star_vacuous < assert contained_in P P.
```
```
Variables: P
H1 : reflexive P
H2 : transitive P
H3 : contained_in P P
============================
contained_in (star P) P

star_vacuous < apply star_minimal to H3 H1 H2.
```
```
Variables: P
H1 : reflexive P
H2 : transitive P
H3 : contained_in P P
H4 : contained_in (star P) P
============================
contained_in (star P) P

star_vacuous < search.
Proof completed.
```
```Abella < Theorem star_idempotent :
forall P, contained_in (star (star P)) (star P).

```
```
============================
forall P, contained_in (star (star P)) (star P)

star_idempotent < intros.
```
```
Variables: P
============================
contained_in (star (star P)) (star P)

star_idempotent < apply star_reflexive with P = P.
```
```
Variables: P
H1 : reflexive (star P)
============================
contained_in (star (star P)) (star P)

star_idempotent < apply star_transitive with P = P.
```
```
Variables: P
H1 : reflexive (star P)
H2 : transitive (star P)
============================
contained_in (star (star P)) (star P)

star_idempotent < apply star_vacuous to H1 H2.
```
```
Variables: P
H1 : reflexive (star P)
H2 : transitive (star P)
H3 : contained_in (star (star P)) (star P)
============================
contained_in (star (star P)) (star P)

star_idempotent < search.
Proof completed.
```
```Abella <
```