enrich
   indexseq, 
   stackseq
with
   
   
   functions  solitaire : list → llist;
              solitaireh : list × llist → llist;
              solix : list → illist;
              solixh : list × nat × illist → illist;
              . .tolist . : illist × list → llist prio 16 right;
              . .tolist . : ilist × list → list prio 16 right;
              push : elem × llist → llist;
              pushx : nat × illist × list → illist;
              maxincseq# : list → nat;
   predicates  inv : illist × nat;
               all< : ilist × nat;
               precedes : nat × nat × list;
               precedes∃ : illist × list;
               ascsubseq : ilist × list;
               ordered : ilist × list;
               ordered : illist × list;
               covers : illist × nat;
               covers : illist × ilist;
   
   

   

   axioms solitaire-def :  ⊦ solitaire(x) = solitaireh(x, []);
          solitaireh-base :  ⊦ solitaireh([], xs) = xs;
          solitaireh-rec :  ⊦ solitaireh(a ' + x, xs) = solitaireh(x, push(a, xs));
          solix-def :  ⊦ solix(x) = solixh(x, 0, []);
          solixh-base :  ⊦ n = # x → solixh(x, n, ixs) = ixs;
          solixh-rec :  ⊦ n < # x → solixh(x, n, ixs) = solixh(x, n + 1, pushx(n, ixs, x));
          push-base :  ⊦ push(a, []) = (a + []) + [];
          push-rec :  ⊦ push(a, x ' + xs) = (¬ x.first < a ⊃ (a + x) + xs;x + push(a, xs));
          pushx-base :  ⊦ pushx(n, [], x) = (n + []) + [];
          pushx-rec :  ⊦ pushx(n, ix ' + ixs, x) = (¬ x[ix.first] < x[n] ⊃ (n + ix) + ixs;ix + pushx(n, ixs, x));
          tolistl-base :  ⊦ ([]).tolist(x) = [];
          tolistl-rec :  ⊦ (ix ' + ixs).tolist(x) = ix.tolist(x) + ixs.tolist(x);
          tolist-base :  ⊦ ([]).tolist(x) = [];
          tolist-rec :  ⊦ (n ' + ix).tolist(x) = x[n] + ix.tolist(x);
          inv-base :  ⊦ inv([], n);
          inv-rec :  ⊦ inv(ix ' + ixs, n) ↔ ix ≠ [] ∧ all<(ix, n) ∧ inv(ixs, n);
          allls-base :  ⊦ all<([], n);
          allls-rec :  ⊦ all<(n0 ' + ix, n) ↔ n0 < n ∧ all<(ix, n);
          orderedl-base :  ⊦ ordered([], x);
          orderedl-rec :  ⊦ ordered(ix ' + ixs, x) ↔ ordered(ix, x) ∧ ordered(ixs, x);
          ordered-base :  ⊦ ordered([], x);
          ordered-rec1 :  ⊦ ordered(n ', x);
          ordered-rec2 :  ⊦ ordered(n0 ' + n1 ' + ix, x) ↔ ordered(n1 ' + ix, x) ∧ n0 > n1 ∧ ¬ x[n1] < x[n0];
          covers-def :  ⊦ covers(ixs, n) ↔ (∀ n0. n0 < n → (∃ m. m < # ixs ∧ n0 ∈ ixs[m]));
          coversi-def :  ⊦ covers(ixs, ix) ↔ (∀ n. n ∈ ix → (∃ m. m < # ixs ∧ n ∈ ixs[m]));
          precedes-def :  ⊦ precedes(n, m, x) ↔ n < m ∧ m < # x ∧ x[n] < x[m];
          precedesex-base :  ⊦ precedes∃([], x);
          precedesex-rec0 :  ⊦ precedes∃(ix ', x);
          precedesex-rec1
          : 
            ⊦   precedes∃(ix0 ' + ix1 ' + ixs, x)
              ↔ precedes∃(ix1 ' + ixs, x) ∧ (∀ n1. n1 ∈ ix1 → (∃ n0. n0 ∈ ix0 ∧ precedes(n0, n1, x)));
          ascsubseq-base :  ⊦ ascsubseq([], x);
          ascsubseq-single :  ⊦ ascsubseq(n ', x) ↔ n < # x;
          ascsubseq-rec :  ⊦ ascsubseq(n ' + m ' + ix, x) ↔ precedes(n, m, x) ∧ ascsubseq(m + ix, x);
          maxincseqno-def
          :  ⊦ maxincseq#(x) = n ↔ (∃ ix. ascsubseq(ix, x) ∧ # ix = n ∧ (∀ ix. ascsubseq(ix, x) → # ix ≤ n))

   

   
end enrich