Welcome to Abella 2.0.4-dev
Abella < Specification "higher-order".
Reading 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 <