thf
  (
    l_e_st_eq_landau_n_rt_rp_satzd199_def
  ,
   definition
  ,
     l_e_st_eq_landau_n_rt_rp_satzd199
    :=
     (
        ^
       [
            Xa
          :
                l_e_st_eq_landau_n_rt_rp_dif
       ]
       :
          ^
         [
              Xb
            :
                  l_e_st_eq_landau_n_rt_rp_dif
         ]
         :
            ^
           [
                Xc
              :
                    l_e_st_eq_landau_n_rt_rp_dif
           ]
           :
            (
                         l_e_st_eq_landau_n_rt_rp_tr3eq
                    @
                     (
                             l_e_st_eq_landau_n_rt_rp_td
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_td
                            @
                                 Xa
                           @
                                Xb
                         )
                       @
                            Xc
                     )
                   @
                    (
                            l_e_st_eq_landau_n_rt_rp_df
                       @
                        (
                                l_e_st_eq_landau_n_rt_rp_pl
                           @
                            (
                                    l_e_st_eq_landau_n_rt_rp_ts
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_pl
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_ts
                                       @
                                        (
                                               l_e_st_eq_landau_n_rt_rp_1a
                                          @
                                               Xa
                                        )
                                      @
                                       (
                                               l_e_st_eq_landau_n_rt_rp_1b
                                          @
                                               Xa
                                         @
                                              Xb
                                       )
                                    )
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_ts
                                      @
                                       (
                                              l_e_st_eq_landau_n_rt_rp_2a
                                         @
                                              Xa
                                       )
                                     @
                                      (
                                              l_e_st_eq_landau_n_rt_rp_2b
                                         @
                                              Xa
                                        @
                                             Xb
                                      )
                                   )
                                )
                              @
                               (
                                        l_e_st_eq_landau_n_rt_rp_1c
                                   @
                                        Xa
                                  @
                                       Xb
                                 @
                                      Xc
                               )
                            )
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_ts
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_pl
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_ts
                                      @
                                       (
                                              l_e_st_eq_landau_n_rt_rp_1a
                                         @
                                              Xa
                                       )
                                     @
                                      (
                                              l_e_st_eq_landau_n_rt_rp_2b
                                         @
                                              Xa
                                        @
                                             Xb
                                      )
                                   )
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_ts
                                     @
                                      (
                                             l_e_st_eq_landau_n_rt_rp_2a
                                        @
                                             Xa
                                      )
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_1b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                  )
                               )
                             @
                              (
                                       l_e_st_eq_landau_n_rt_rp_2c
                                  @
                                       Xa
                                 @
                                      Xb
                                @
                                     Xc
                              )
                           )
                        )
                      @
                       (
                               l_e_st_eq_landau_n_rt_rp_pl
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_ts
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_pl
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_ts
                                      @
                                       (
                                              l_e_st_eq_landau_n_rt_rp_1a
                                         @
                                              Xa
                                       )
                                     @
                                      (
                                              l_e_st_eq_landau_n_rt_rp_1b
                                         @
                                              Xa
                                        @
                                             Xb
                                      )
                                   )
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_ts
                                     @
                                      (
                                             l_e_st_eq_landau_n_rt_rp_2a
                                        @
                                             Xa
                                      )
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_2b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                  )
                               )
                             @
                              (
                                       l_e_st_eq_landau_n_rt_rp_2c
                                  @
                                       Xa
                                 @
                                      Xb
                                @
                                     Xc
                              )
                           )
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_ts
                             @
                              (
                                      l_e_st_eq_landau_n_rt_rp_pl
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_ts
                                     @
                                      (
                                             l_e_st_eq_landau_n_rt_rp_1a
                                        @
                                             Xa
                                      )
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_2b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                  )
                                @
                                 (
                                         l_e_st_eq_landau_n_rt_rp_ts
                                    @
                                     (
                                            l_e_st_eq_landau_n_rt_rp_2a
                                       @
                                            Xa
                                     )
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_1b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                 )
                              )
                            @
                             (
                                      l_e_st_eq_landau_n_rt_rp_1c
                                 @
                                      Xa
                                @
                                     Xb
                               @
                                    Xc
                             )
                          )
                       )
                    )
                  @
                   (
                           l_e_st_eq_landau_n_rt_rp_df
                      @
                       (
                               l_e_st_eq_landau_n_rt_rp_pl
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_ts
                              @
                               (
                                      l_e_st_eq_landau_n_rt_rp_1a
                                 @
                                      Xa
                               )
                             @
                              (
                                      l_e_st_eq_landau_n_rt_rp_pl
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_ts
                                     @
                                      (
                                              l_e_st_eq_landau_n_rt_rp_1b
                                         @
                                              Xa
                                        @
                                             Xb
                                      )
                                    @
                                     (
                                              l_e_st_eq_landau_n_rt_rp_1c
                                         @
                                              Xa
                                        @
                                             Xb
                                       @
                                            Xc
                                     )
                                  )
                                @
                                 (
                                         l_e_st_eq_landau_n_rt_rp_ts
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_2b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                   @
                                    (
                                             l_e_st_eq_landau_n_rt_rp_2c
                                        @
                                             Xa
                                       @
                                            Xb
                                      @
                                           Xc
                                    )
                                 )
                              )
                           )
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_ts
                             @
                              (
                                     l_e_st_eq_landau_n_rt_rp_2a
                                @
                                     Xa
                              )
                            @
                             (
                                     l_e_st_eq_landau_n_rt_rp_pl
                                @
                                 (
                                         l_e_st_eq_landau_n_rt_rp_ts
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_1b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                   @
                                    (
                                             l_e_st_eq_landau_n_rt_rp_2c
                                        @
                                             Xa
                                       @
                                            Xb
                                      @
                                           Xc
                                    )
                                 )
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_ts
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_2b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                  @
                                   (
                                            l_e_st_eq_landau_n_rt_rp_1c
                                       @
                                            Xa
                                      @
                                           Xb
                                     @
                                          Xc
                                   )
                                )
                             )
                          )
                       )
                     @
                      (
                              l_e_st_eq_landau_n_rt_rp_pl
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_ts
                             @
                              (
                                     l_e_st_eq_landau_n_rt_rp_1a
                                @
                                     Xa
                              )
                            @
                             (
                                     l_e_st_eq_landau_n_rt_rp_pl
                                @
                                 (
                                         l_e_st_eq_landau_n_rt_rp_ts
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_1b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                   @
                                    (
                                             l_e_st_eq_landau_n_rt_rp_2c
                                        @
                                             Xa
                                       @
                                            Xb
                                      @
                                           Xc
                                    )
                                 )
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_ts
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_2b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                  @
                                   (
                                            l_e_st_eq_landau_n_rt_rp_1c
                                       @
                                            Xa
                                      @
                                           Xb
                                     @
                                          Xc
                                   )
                                )
                             )
                          )
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_ts
                            @
                             (
                                    l_e_st_eq_landau_n_rt_rp_2a
                               @
                                    Xa
                             )
                           @
                            (
                                    l_e_st_eq_landau_n_rt_rp_pl
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_ts
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_1b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                  @
                                   (
                                            l_e_st_eq_landau_n_rt_rp_1c
                                       @
                                            Xa
                                      @
                                           Xb
                                     @
                                          Xc
                                   )
                                )
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_ts
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_2b
                                      @
                                           Xa
                                     @
                                          Xb
                                   )
                                 @
                                  (
                                           l_e_st_eq_landau_n_rt_rp_2c
                                      @
                                           Xa
                                     @
                                          Xb
                                    @
                                         Xc
                                  )
                               )
                            )
                         )
                      )
                   )
                 @
                  (
                          l_e_st_eq_landau_n_rt_rp_td
                     @
                          Xa
                    @
                     (
                             l_e_st_eq_landau_n_rt_rp_td
                        @
                             Xb
                       @
                            Xc
                     )
                  )
                @
                 (
                          l_e_st_eq_landau_n_rt_rp_tdeq2a
                     @
                          Xc
                    @
                     (
                             l_e_st_eq_landau_n_rt_rp_pl
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_ts
                            @
                             (
                                    l_e_st_eq_landau_n_rt_rp_1a
                               @
                                    Xa
                             )
                           @
                            (
                                    l_e_st_eq_landau_n_rt_rp_1b
                               @
                                    Xa
                              @
                                   Xb
                            )
                         )
                       @
                        (
                                l_e_st_eq_landau_n_rt_rp_ts
                           @
                            (
                                   l_e_st_eq_landau_n_rt_rp_2a
                              @
                                   Xa
                            )
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_2b
                              @
                                   Xa
                             @
                                  Xb
                           )
                        )
                     )
                   @
                    (
                            l_e_st_eq_landau_n_rt_rp_pl
                       @
                        (
                                l_e_st_eq_landau_n_rt_rp_ts
                           @
                            (
                                   l_e_st_eq_landau_n_rt_rp_1a
                              @
                                   Xa
                            )
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_2b
                              @
                                   Xa
                             @
                                  Xb
                           )
                        )
                      @
                       (
                               l_e_st_eq_landau_n_rt_rp_ts
                          @
                           (
                                  l_e_st_eq_landau_n_rt_rp_2a
                             @
                                  Xa
                           )
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_1b
                             @
                                  Xa
                            @
                                 Xb
                          )
                       )
                    )
                 )
               @
                (
                            l_e_st_eq_landau_n_rt_rp_eqsmsd
                       @
                        (
                                l_e_st_eq_landau_n_rt_rp_pl
                           @
                            (
                                    l_e_st_eq_landau_n_rt_rp_ts
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_pl
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_ts
                                       @
                                        (
                                               l_e_st_eq_landau_n_rt_rp_1a
                                          @
                                               Xa
                                        )
                                      @
                                       (
                                               l_e_st_eq_landau_n_rt_rp_1b
                                          @
                                               Xa
                                         @
                                              Xb
                                       )
                                    )
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_ts
                                      @
                                       (
                                              l_e_st_eq_landau_n_rt_rp_2a
                                         @
                                              Xa
                                       )
                                     @
                                      (
                                              l_e_st_eq_landau_n_rt_rp_2b
                                         @
                                              Xa
                                        @
                                             Xb
                                      )
                                   )
                                )
                              @
                               (
                                        l_e_st_eq_landau_n_rt_rp_1c
                                   @
                                        Xa
                                  @
                                       Xb
                                 @
                                      Xc
                               )
                            )
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_ts
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_pl
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_ts
                                      @
                                       (
                                              l_e_st_eq_landau_n_rt_rp_1a
                                         @
                                              Xa
                                       )
                                     @
                                      (
                                              l_e_st_eq_landau_n_rt_rp_2b
                                         @
                                              Xa
                                        @
                                             Xb
                                      )
                                   )
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_ts
                                     @
                                      (
                                             l_e_st_eq_landau_n_rt_rp_2a
                                        @
                                             Xa
                                      )
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_1b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                  )
                               )
                             @
                              (
                                       l_e_st_eq_landau_n_rt_rp_2c
                                  @
                                       Xa
                                 @
                                      Xb
                                @
                                     Xc
                              )
                           )
                        )
                      @
                       (
                               l_e_st_eq_landau_n_rt_rp_pl
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_ts
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_pl
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_ts
                                      @
                                       (
                                              l_e_st_eq_landau_n_rt_rp_1a
                                         @
                                              Xa
                                       )
                                     @
                                      (
                                              l_e_st_eq_landau_n_rt_rp_1b
                                         @
                                              Xa
                                        @
                                             Xb
                                      )
                                   )
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_ts
                                     @
                                      (
                                             l_e_st_eq_landau_n_rt_rp_2a
                                        @
                                             Xa
                                      )
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_2b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                  )
                               )
                             @
                              (
                                       l_e_st_eq_landau_n_rt_rp_2c
                                  @
                                       Xa
                                 @
                                      Xb
                                @
                                     Xc
                              )
                           )
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_ts
                             @
                              (
                                      l_e_st_eq_landau_n_rt_rp_pl
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_ts
                                     @
                                      (
                                             l_e_st_eq_landau_n_rt_rp_1a
                                        @
                                             Xa
                                      )
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_2b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                  )
                                @
                                 (
                                         l_e_st_eq_landau_n_rt_rp_ts
                                    @
                                     (
                                            l_e_st_eq_landau_n_rt_rp_2a
                                       @
                                            Xa
                                     )
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_1b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                 )
                              )
                            @
                             (
                                      l_e_st_eq_landau_n_rt_rp_1c
                                 @
                                      Xa
                                @
                                     Xb
                               @
                                    Xc
                             )
                          )
                       )
                     @
                      (
                              l_e_st_eq_landau_n_rt_rp_pl
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_ts
                             @
                              (
                                     l_e_st_eq_landau_n_rt_rp_1a
                                @
                                     Xa
                              )
                            @
                             (
                                     l_e_st_eq_landau_n_rt_rp_pl
                                @
                                 (
                                         l_e_st_eq_landau_n_rt_rp_ts
                                    @
                                     (
                                             l_e_st_eq_landau_n_rt_rp_1b
                                        @
                                             Xa
                                       @
                                            Xb
                                     )
                                   @
                                    (
                                             l_e_st_eq_landau_n_rt_rp_1c
                                        @
                                             Xa
                                       @
                                            Xb
                                      @
                                           Xc
                                    )
                                 )
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_ts
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_2b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                  @
                                   (
                                            l_e_st_eq_landau_n_rt_rp_2c
                                       @
                                            Xa
                                      @
                                           Xb
                                     @
                                          Xc
                                   )
                                )
                             )
                          )
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_ts
                            @
                             (
                                    l_e_st_eq_landau_n_rt_rp_2a
                               @
                                    Xa
                             )
                           @
                            (
                                    l_e_st_eq_landau_n_rt_rp_pl
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_ts
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_1b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                  @
                                   (
                                            l_e_st_eq_landau_n_rt_rp_2c
                                       @
                                            Xa
                                      @
                                           Xb
                                     @
                                          Xc
                                   )
                                )
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_ts
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_2b
                                      @
                                           Xa
                                     @
                                          Xb
                                   )
                                 @
                                  (
                                           l_e_st_eq_landau_n_rt_rp_1c
                                      @
                                           Xa
                                     @
                                          Xb
                                    @
                                         Xc
                                  )
                               )
                            )
                         )
                      )
                    @
                     (
                             l_e_st_eq_landau_n_rt_rp_pl
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_ts
                            @
                             (
                                    l_e_st_eq_landau_n_rt_rp_1a
                               @
                                    Xa
                             )
                           @
                            (
                                    l_e_st_eq_landau_n_rt_rp_pl
                               @
                                (
                                        l_e_st_eq_landau_n_rt_rp_ts
                                   @
                                    (
                                            l_e_st_eq_landau_n_rt_rp_1b
                                       @
                                            Xa
                                      @
                                           Xb
                                    )
                                  @
                                   (
                                            l_e_st_eq_landau_n_rt_rp_2c
                                       @
                                            Xa
                                      @
                                           Xb
                                     @
                                          Xc
                                   )
                                )
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_ts
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_2b
                                      @
                                           Xa
                                     @
                                          Xb
                                   )
                                 @
                                  (
                                           l_e_st_eq_landau_n_rt_rp_1c
                                      @
                                           Xa
                                     @
                                          Xb
                                    @
                                         Xc
                                  )
                               )
                            )
                         )
                       @
                        (
                                l_e_st_eq_landau_n_rt_rp_ts
                           @
                            (
                                   l_e_st_eq_landau_n_rt_rp_2a
                              @
                                   Xa
                            )
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_pl
                              @
                               (
                                       l_e_st_eq_landau_n_rt_rp_ts
                                  @
                                   (
                                           l_e_st_eq_landau_n_rt_rp_1b
                                      @
                                           Xa
                                     @
                                          Xb
                                   )
                                 @
                                  (
                                           l_e_st_eq_landau_n_rt_rp_1c
                                      @
                                           Xa
                                     @
                                          Xb
                                    @
                                         Xc
                                  )
                               )
                             @
                              (
                                      l_e_st_eq_landau_n_rt_rp_ts
                                 @
                                  (
                                          l_e_st_eq_landau_n_rt_rp_2b
                                     @
                                          Xa
                                    @
                                         Xb
                                  )
                                @
                                 (
                                          l_e_st_eq_landau_n_rt_rp_2c
                                     @
                                          Xa
                                    @
                                         Xb
                                   @
                                        Xc
                                 )
                              )
                           )
                        )
                     )
                   @
                    (
                                l_e_st_eq_landau_n_rt_rp_4d199_t3
                           @
                            (
                                   l_e_st_eq_landau_n_rt_rp_1a
                              @
                                   Xa
                            )
                          @
                           (
                                  l_e_st_eq_landau_n_rt_rp_2a
                             @
                                  Xa
                           )
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_1b
                             @
                                  Xa
                            @
                                 Xb
                          )
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_2b
                            @
                                 Xa
                           @
                                Xb
                         )
                       @
                        (
                                 l_e_st_eq_landau_n_rt_rp_1c
                            @
                                 Xa
                           @
                                Xb
                          @
                               Xc
                        )
                      @
                       (
                                l_e_st_eq_landau_n_rt_rp_2c
                           @
                                Xa
                          @
                               Xb
                         @
                              Xc
                       )
                    )
                  @
                   (
                               l_e_st_eq_landau_n_rt_rp_4d199_t3
                          @
                           (
                                  l_e_st_eq_landau_n_rt_rp_1a
                             @
                                  Xa
                           )
                         @
                          (
                                 l_e_st_eq_landau_n_rt_rp_2a
                            @
                                 Xa
                          )
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_1b
                            @
                                 Xa
                           @
                                Xb
                         )
                       @
                        (
                                l_e_st_eq_landau_n_rt_rp_2b
                           @
                                Xa
                          @
                               Xb
                        )
                      @
                       (
                                l_e_st_eq_landau_n_rt_rp_2c
                           @
                                Xa
                          @
                               Xb
                         @
                              Xc
                       )
                     @
                      (
                               l_e_st_eq_landau_n_rt_rp_1c
                          @
                               Xa
                         @
                              Xb
                        @
                             Xc
                      )
                   )
                )
              @
               (
                        l_e_st_eq_landau_n_rt_rp_tdeq1b
                   @
                        Xa
                  @
                   (
                           l_e_st_eq_landau_n_rt_rp_pl
                      @
                       (
                               l_e_st_eq_landau_n_rt_rp_ts
                          @
                           (
                                   l_e_st_eq_landau_n_rt_rp_1b
                              @
                                   Xa
                             @
                                  Xb
                           )
                         @
                          (
                                   l_e_st_eq_landau_n_rt_rp_1c
                              @
                                   Xa
                             @
                                  Xb
                            @
                                 Xc
                          )
                       )
                     @
                      (
                              l_e_st_eq_landau_n_rt_rp_ts
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_2b
                             @
                                  Xa
                            @
                                 Xb
                          )
                        @
                         (
                                  l_e_st_eq_landau_n_rt_rp_2c
                             @
                                  Xa
                            @
                                 Xb
                           @
                                Xc
                         )
                      )
                   )
                 @
                  (
                          l_e_st_eq_landau_n_rt_rp_pl
                     @
                      (
                              l_e_st_eq_landau_n_rt_rp_ts
                         @
                          (
                                  l_e_st_eq_landau_n_rt_rp_1b
                             @
                                  Xa
                            @
                                 Xb
                          )
                        @
                         (
                                  l_e_st_eq_landau_n_rt_rp_2c
                             @
                                  Xa
                            @
                                 Xb
                           @
                                Xc
                         )
                      )
                    @
                     (
                             l_e_st_eq_landau_n_rt_rp_ts
                        @
                         (
                                 l_e_st_eq_landau_n_rt_rp_2b
                            @
                                 Xa
                           @
                                Xb
                         )
                       @
                        (
                                 l_e_st_eq_landau_n_rt_rp_1c
                            @
                                 Xa
                           @
                                Xb
                          @
                               Xc
                        )
                     )
                  )
               )
            )
     )
   
  )
  .