Solve-Aux {
  /* В начале системы уравнение вида T E : Lt Le  */
  (e.UsedVars) (e.Contrs) ((t.Pt e.Pe) ':' (t.Ht e.He)) e.Equations (e.Assigns)
    , <IsTerm t.Ht> : True
    , <IsTerm t.Pt> : True
    = <Solve-TermEquation
        (e.UsedVars)
        t.Pt t.Ht
        (e.Contrs) ((e.Pe) ':' (e.He)) e.Equations (e.Assigns)
      > : {
        Success e.PRTC = <Solve-Aux e.PRTC>;
        Failure =
      };

  /* В начале системы уравнение вида E T: Le Lt */
  (e.UsedVars) (e.Contrs) ((e.Pe t.Pt) ':' (e.He t.Ht)) e.Equations (e.Assigns)
    , <IsTerm t.Ht> : True
    , <IsTerm t.Pt> : True
    = <Solve-TermEquation
        (e.UsedVars)
        t.Pt t.Ht
        (e.Contrs) ((e.Pe) ':' (e.He)) e.Equations (e.Assigns)
      > : {
        Success e.PRTC = <Solve-Aux e.PRTC>;
        Failure =
      };

  /* Уравнения вида e.x E : Lt Le
     Разделяем на две независимые системы
     e.x -> empty
     e.x -> t.N e.N+1
  */
  (e.UsedVars) (e.Contrs) ((t.Pt e.Pe) ':' (t.Ht e.He))
  e.Equations (e.Assigns)
    , <IsTerm t.Ht> : True
    , t.Pt : (TkVariable 'e' e.Index)
    = <NewVarName (e.UsedVars) 't' 0 ()> : (e.UsedVars^) 't' e.tIdx
    = <NewVarName (e.UsedVars) 'e' 0 ()> : (e.UsedVars^) 'e' e.eIdx
    = <AddContraction
        (t.Pt ':' )
        (e.Contrs)
        ((e.Pe) ':' (t.Ht e.He)) e.Equations
        (e.Assigns)
      > : e.Branch1
    = <AddContraction
        (t.Pt ':' (TkVariable 't' e.tIdx) (TkVariable 'e' e.eIdx))
        (e.Contrs)
        ((t.Pt e.Pe) ':' (t.Ht e.He)) e.Equations
        (e.Assigns)
      >: e.Branch2
    = <Solve-Aux
        (e.UsedVars)
        e.Branch1
      >
      <Solve-Aux
        (e.UsedVars)
        e.Branch2
      >;

  /* Уравнения вида E e.x : Le Lt
     Разделяем на две независимые системы
     e.x -> empty
     e.x -> e.N+1 t.N
  */
  (e.UsedVars) (e.Contrs) ((e.Pe t.Pt) ':' (e.He t.Ht))
  e.Equations (e.Assigns)
    , <IsTerm t.Ht> : True
    , t.Pt : (TkVariable 'e' e.Index)
      = <NewVarName (e.UsedVars) 't' 0 ()> : (e.UsedVars^) 't' e.tIdx
      = <NewVarName (e.UsedVars) 'e' 0 ()> : (e.UsedVars^) 'e' e.eIdx
      = <AddContraction
          (t.Pt ':' )
          (e.Contrs)
          ((e.Pe) ':' (e.He t.Ht)) e.Equations
          (e.Assigns)
        > : e.Branch1
      = <AddContraction
          (t.Pt ':' (TkVariable 'e' e.eIdx) (TkVariable 't' e.tIdx))
          (e.Contrs)
          ((e.Pe t.Pt) ':' (e.He t.Ht)) e.Equations
          (e.Assigns)
        >: e.Branch2
      = <Solve-Aux
          (e.UsedVars)
          e.Branch1
        >

        <Solve-Aux
          (e.UsedVars)
          e.Branch2
        >;

  /* Если уравнение имеет вид Expr: e.x, добавляем присванивание
     вида Expr <- e.x */
  (e.UsedVars) (e.Contrs) ((e.Pe) ':' ((TkVariable 'e' e.Idx)))
  e.Equations (e.Assigns)
    = <Solve-Aux
        (e.UsedVars)
        (e.Contrs)
        e.Equations
        (e.Assigns (e.Pe ':' (TkVariable 'e' e.Idx)))
      >;

  /* Если уравнение имеет вид empty: Lt Le, ничего не возвращаем */
  (e.UsedVars) (e.Contrs) (() ':' (t.Ht e.He)) e.Equations (e.Assigns)
    , <IsTerm t.Ht>: True = ;

  /* Если уравнение имеет вид e.i* : empty, возвращаем результат,
     предварительно добавив пустые сужения
  */
  (e.UsedVars) (e.Contrs) ((e.Pt) ':' ()) e.Equations (e.Assigns)
    , <IsFreeVariableSeq e.Pt> : True
    , <Map
        {
            t.Free = (t.Free ':' )
        }
        e.Pt
      > : e.NewContrs
    = <Solve-Aux
        (e.UsedVars)
        <AddContractions
          (e.NewContrs)
          (e.Contrs)
          e.Equations
          (e.Assigns)
        >
      >;

  (e.UsedVars) (e.Contrs) (() ':' ()) e.Equations (e.Assigns) =
    <Solve-Aux (e.UsedVars) (e.Contrs) e.Equations (e.Assigns)>;

  (e.UsedVars) (e.Contrs) (e.Assigns) = <Prout 'CONTRS:' e.Contrs 'ASGNS:' e.Assigns> <Solution-PostProcess (e.Contrs) (e.Assigns)>;

  e.Other = Undefined
}


/*
  Решает уравнение вида P:H для термов

  <Solve-TermEquation (e.UsedVars) t.Symbol1 t.Symbol2 e.PRTC>
    == t.Result

    t.Result ::= Success t.PRTC | Failure
    e.PRTC :: = (t.Contrs*) t.Equations* (t.Assigns*)

    PRTC - partially resolved term clash
*/

Solve-TermEquation {
  /* H является символом */
  (e.UsedVars) t.Symbol t.Symbol e.PRTC
    , t.Symbol : (Symbol s.Type e.Info)
    = Success (e.UsedVars) e.PRTC
  /* нет подстановок, нет сужений */;

  /* P - символ, H - s-переменная */
  (e.UsedVars) t.Symbol t.Svar (e.Contrs) e.Equations (e.Assigns)
    , t.Symbol t.Svar
    : (Symbol s.Type e.Info) (TkVariable 's' e.Hindex)
    = Success
      (e.UsedVars)
      (e.Contrs) e.Equations
      (e.Assigns (t.Symbol ':' t.Svar));

  /* P - s-переменная, H - s-переменная */
  (e.UsedVars) t.PSvar t.HSvar (e.Contrs) e.Equations (e.Assigns)
    , t.PSvar t.HSvar
    : (TkVariable 's' e.Pindex) (TkVariable 's' e.Hindex)
    = Success
      (e.UsedVars)
      (e.Contrs)
      e.Equations
      (e.Assigns (t.PSvar ':' t.HSvar));


  /* P - s-переменная, H - символ */
  (e.UsedVars) t.Svar t.Symbol (e.Contrs) e.Equations (e.Assigns)
    , t.Svar : (TkVariable 's' e.Pindex)
    , <IsSVarSubset t.Symbol> : True
    = Success
      (e.UsedVars)
      <AddContraction
        (t.Svar ':' t.Symbol)
        (e.Contrs)
        e.Equations
        (e.Assigns)
      >;

  /* P - терм, H - t-переменная */
  (e.UsedVars) t.PVar t.HVar (e.Contrs) e.Equations (e.Assigns)
    , t.HVar: (TkVariable 't' e.Tindex)
    = Success
      (e.UsedVars)
      (e.Contrs)
      e.Equations
      (e.Assigns (t.PVar':'(TkVariable 't' e.Tindex)));

  /* P - t-переменная, H - скобочный терм */
  (e.UsedVars) t.PTvar (Brackets e.HBody) (e.Contrs) e.Equations (e.Assigns)
    , t.PTvar : (TkVariable 't' e.Pindex)
    = <NewVarName (e.UsedVars) 'e' 0 ()>
      : t.NewVars e.NewIndex
      = Success
        t.NewVars
        <AddContraction
          (t.PTvar ':' (Brackets (TkVariable 'e' e.NewIndex)))
          (e.Contrs)
          e.Equations (((TkVariable 'e' e.NewIndex)) ':' (e.HBody))
          (e.Assigns)
        >;

  /* P - t-переменная, H - символ */
  (e.UsedVars) t.PTvar t.Symbol (e.Contrs) e.Equations (e.Assigns)
    , t.PTvar t.Symbol
    : (TkVariable 't' e.Pindex) (Symbol s.Type e.Info)
    = Success
      (e.UsedVars)
      <AddContraction
        (t.PTvar ':' t.Symbol)
        (e.Contrs)
        e.Equations
        (e.Assigns)
      >;

  /* P - t-переменная, H - s-переменная */
  (e.UsedVars) t.PTvar t.HSvar (e.Contrs) e.Equations (e.Assigns)
    , t.PTvar t.HSvar
    : (TkVariable 't' e.Pindex) (TkVariable 's' e.Hindex)
    = Success
      (e.UsedVars)
      <AddContraction
        (t.PTvar ':' t.HSvar)
        (e.Contrs)
        e.Equations
        (e.Assigns)
      >;

  /* H является (H′) */
  (e.UsedVars)
  (Brackets e.TBody)(Brackets e.HBody)
  (e.Contrs) e.Equations (e.Assigns)
    = Success
      (e.UsedVars)
      (e.Contrs) e.Equations ((e.TBody) ':' (e.HBody))
      (e.Assigns);

  /* H является [H′] */
  (e.UsedVars)
  (ADT-Brackets (e.Name) e.TBody)(ADT-Brackets (e.Name) e.HBody)
  (e.Contrs) e.Equations (e.Assigns)
    = Success
      (e.UsedVars)
      (e.Contrs) e.Equations ((e.TBody) ':' (e.HBody)) (e.Assigns);

  e.Other = Failure
}