ahahahahomg

d-mp
(d-⊤-i program
 (nd
  (◇-hs
   (∧-e1
    (identity
     ((at (l (s zero)) ⊃ ◇ (▢ (¬ (var (bvar zero))))) ∧
      (▢ (¬ (var (bvar zero))) ⊃ ◇ (after (l (s (s zero))))))))
   (∧-e2
    (identity
     ((at (l (s zero)) ⊃ ◇ (▢ (¬ (var (bvar zero))))) ∧
      (▢ (¬ (var (bvar zero))) ⊃ ◇ (after (l (s (s zero)))))))))))
(d-∧-i
 (d-mp
  (d-⊤-i program
   (nd
    (hs
     (∧-e1
      (identity
       ((at (l (s zero)) ⊃
         ◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))
        ∧
        (◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))) ⊃
         ◇ (▢ (¬ (var (bvar zero))))))))
     (∧-e2
      (identity
       ((at (l (s zero)) ⊃
         ◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))
        ∧
        (◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))) ⊃
         ◇ (▢ (¬ (var (bvar zero)))))))))))
  (d-∧-i
   (d-mp
    (d-⊤-i program
     (nd
      (hs
       (∧-e1
        (identity
         ((at (l (s zero)) ⊃
           (▢
            ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
             ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
            ∧ ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))
          ∧
          ((▢
            ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
             ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
            ∧ ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
           ⊃ ◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))))))
       (∧-e2
        (identity
         ((at (l (s zero)) ⊃
           (▢
            ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
             ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
            ∧ ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))
          ∧
          ((▢
            ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
             ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
            ∧ ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
           ⊃ ◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))))))))
    (d-∧-i
     (d-mp
      (d-⊤-i program
       (nd
        (⊃-comb
         (∧-e1
          (identity
           ((at (l (s zero)) ⊃
             ▢
             ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
              ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))
            ∧
            (at (l (s zero)) ⊃ ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))))
         (∧-e2
          (identity
           ((at (l (s zero)) ⊃
             ▢
             ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
              ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))
            ∧
            (at (l (s zero)) ⊃
             ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero))))))))))
      (d-∧-i
       (d-mp
        (d-⊤-i program
         (nd
          (imp-eq2
           (∨-i2
            (identity
             (▢
              ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
               ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))))
            (¬ (at (l (s zero))))))))
        (▢-i program (after (l (s zero)) ∧ ¬ (var (bvar zero)))))
       (d-mp
        (d-⊤-i program
         (nd
          (TL12
           (identity
            (at (l (s zero)) ~> (after (l (s zero)) ∧ ¬ (var (bvar zero))))))))
        (asr-f program (l (s zero)) (bvar zero)))))
     (d-⊤-i program
      (nd
       (◇-mp
        (∧-e1
         (identity
          (▢
           ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
            ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
           ∧ ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero))))))
        (∧-e2
         (identity
          (▢
           ((after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
            ▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))))
           ∧ ◇ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))))))))
   (d-mp
    (d-⊤-i program
     (nd
      (weaken
       (◇-mp
        (∧-e1
         (identity
          (▢
           (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
            ▢ (¬ (var (bvar zero))))
           ∧ ◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))))
        (∧-e2
         (identity
          (▢
           (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero))) ⊃
            ▢ (¬ (var (bvar zero))))
           ∧ ◇ (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))))))))
    (d-⊤-i program
     (▢-⊤
      (nd
       (∧-e2
        (TL4
         (identity (▢ (after (l (s zero)) ∧ ¬ (var (bvar zero)))))))))))))
 (d-mp
  (d-⊤-i program
   (nd
    (weaken
     (mp
      (mp
       (⊤-i
        (nd
         (weaken
          (ca
           (∧-e1
            (∧-e1
             (identity
              (((inside (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))) ∧
                (after (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))))
               ∧ (inside (l (s (s zero))) ∨ after (l (s (s zero))))))))
           (∧-e2
            (∧-e1
             (identity
              (((inside (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))) ∧
                (after (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))))
               ∧ (inside (l (s (s zero))) ∨ after (l (s (s zero))))))))
           (∧-e2
            (identity
             (((inside (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))) ∧
               (after (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))))
              ∧ (inside (l (s (s zero))) ∨ after (l (s (s zero))))))))))
        ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
             ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
            ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
           ∧
           ▢
           ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
            ◇ (after (l (s (s zero))))))
          ∧
          (inside (l (s (s zero))) ⊃
           (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
         ∧ ▢ (¬ (var (bvar zero)))))
       (∧-i
        (hs
         (∧-e2
          (∧-e1
           (identity
            ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                 ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
               ∧
               ▢
               ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                ◇ (after (l (s (s zero))))))
              ∧
              (inside (l (s (s zero))) ⊃
               (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
             ∧ ▢ (¬ (var (bvar zero)))))))
         (mp
          (⊤-i
           (nd
            (weaken
             (ca
              (∧-e1
               (∧-e1
                (identity
                 (((at (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))) ∧
                   (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s zero))))))
                  ∧ (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))))
              (∧-e2
               (∧-e1
                (identity
                 (((at (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))) ∧
                   (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s zero))))))
                  ∧ (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))))
              (∧-e2
               (identity
                (((at (l (s (s zero))) ⊃ ◇ (after (l (s (s zero))))) ∧
                  (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s zero))))))
                 ∧ (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))))))
           ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
               ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
              ∧
              ▢
              ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
               ◇ (after (l (s (s zero))))))
             ∧
             (inside (l (s (s zero))) ⊃
              (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
            ∧ ▢ (¬ (var (bvar zero)))))
          (∧-i
           (mp
            (⊤-i
             (nd
              (weaken
               (mp
                (▢-e
                 (∧-e1
                  (∧-e1
                   (identity
                    ((▢
                      ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                       ◇ (after (l (s (s zero)))))
                      ∧ ▢ (¬ (var (bvar zero))))
                     ∧ at (l (s (s zero))))))))
                (∧-i
                 (∧-e2
                  (identity
                   ((▢
                     ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                      ◇ (after (l (s (s zero)))))
                     ∧ ▢ (¬ (var (bvar zero))))
                    ∧ at (l (s (s zero))))))
                 (∧-e2
                  (∧-e1
                   (identity
                    ((▢
                      ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                       ◇ (after (l (s (s zero)))))
                      ∧ ▢ (¬ (var (bvar zero))))
                     ∧ at (l (s (s zero)))))))))))
             ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                  ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                 ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                ∧
                ▢
                ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                 ◇ (after (l (s (s zero))))))
               ∧
               (inside (l (s (s zero))) ⊃
                (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
              ∧ ▢ (¬ (var (bvar zero)))))
            (∧-i
             (∧-e2
              (∧-e1
               (∧-e1
                (identity
                 ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                      ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                     ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                    ∧
                    ▢
                    ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                     ◇ (after (l (s (s zero))))))
                   ∧
                   (inside (l (s (s zero))) ⊃
                    (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
                  ∧ ▢ (¬ (var (bvar zero))))))))
             (∧-e2
              (identity
               ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                    ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                   ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                  ∧
                  ▢
                  ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                   ◇ (after (l (s (s zero))))))
                 ∧
                 (inside (l (s (s zero))) ⊃
                  (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
                ∧ ▢ (¬ (var (bvar zero))))))))
           (◇-hs
            (hs
             (∧-e2
              (∧-e1
               (∧-e1
                (∧-e1
                 (identity
                  ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                       ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                      ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                     ∧
                     ▢
                     ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                      ◇ (after (l (s (s zero))))))
                    ∧
                    (inside (l (s (s zero))) ⊃
                     (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
                   ∧ ▢ (¬ (var (bvar zero)))))))))
             (mp
              (⊤-i
               (nd
                (weaken
                 (◇-mp
                  (∧-e1
                   (identity
                    (▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))) ∧
                     ◇ (after (l (s (s (s zero))))))))
                  (∧-e2
                   (identity
                    (▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))) ∧
                     ◇ (after (l (s (s (s zero)))))))))))
               ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                    ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                   ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                  ∧
                  ▢
                  ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                   ◇ (after (l (s (s zero))))))
                 ∧
                 (inside (l (s (s zero))) ⊃
                  (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
                ∧ ▢ (¬ (var (bvar zero)))))
              (∧-e2
               (∧-e1
                (∧-e1
                 (∧-e1
                  (∧-e1
                   (identity
                    ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                         ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                        ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                       ∧
                       ▢
                       ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                        ◇ (after (l (s (s zero))))))
                      ∧
                      (inside (l (s (s zero))) ⊃
                       (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
                     ∧ ▢ (¬ (var (bvar zero))))))))))))
            (mp
             (⊤-i
              (nd
               (weaken
                (mp
                 (▢-e
                  (∧-e1
                   (∧-e1
                    (identity
                     ((▢
                       ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                        ◇ (after (l (s (s zero)))))
                       ∧ ▢ (¬ (var (bvar zero))))
                      ∧ at (l (s (s zero))))))))
                 (∧-i
                  (∧-e2
                   (identity
                    ((▢
                      ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                       ◇ (after (l (s (s zero)))))
                      ∧ ▢ (¬ (var (bvar zero))))
                     ∧ at (l (s (s zero))))))
                  (∧-e2
                   (∧-e1
                    (identity
                     ((▢
                       ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                        ◇ (after (l (s (s zero)))))
                       ∧ ▢ (¬ (var (bvar zero))))
                      ∧ at (l (s (s zero)))))))))))
              ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                   ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                  ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                 ∧
                 ▢
                 ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                  ◇ (after (l (s (s zero))))))
                ∧
                (inside (l (s (s zero))) ⊃
                 (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
               ∧ ▢ (¬ (var (bvar zero)))))
             (∧-i
              (∧-e2
               (∧-e1
                (∧-e1
                 (identity
                  ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                       ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                      ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                     ∧
                     ▢
                     ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                      ◇ (after (l (s (s zero))))))
                    ∧
                    (inside (l (s (s zero))) ⊃
                     (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
                   ∧ ▢ (¬ (var (bvar zero))))))))
              (∧-e2
               (identity
                ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                     ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                    ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
                   ∧
                   ▢
                   ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                    ◇ (after (l (s (s zero))))))
                  ∧
                  (inside (l (s (s zero))) ⊃
                   (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
                 ∧ ▢ (¬ (var (bvar zero))))))))))))
        (⊤-i (nd (◇-i (identity (after (l (s (s zero)))))))
         ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
              ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
             ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
            ∧
            ▢
            ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
             ◇ (after (l (s (s zero))))))
           ∧
           (inside (l (s (s zero))) ⊃
            (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
          ∧ ▢ (¬ (var (bvar zero)))))))
      (∧-e1
       (∧-e1
        (∧-e1
         (∧-e1
          (∧-e1
           (identity
            ((((((inside (l (s (s zero))) ∨ after (l (s (s zero)))) ∧
                 ▢ (after (l (s (s (s zero)))) ⊃ at (l (s (s zero)))))
                ∧ (at (l (s (s (s zero)))) ⊃ ◇ (after (l (s (s (s zero)))))))
               ∧
               ▢
               ((at (l (s (s zero))) ∧ ▢ (¬ (var (bvar zero)))) ⊃
                ◇ (after (l (s (s zero))))))
              ∧
              (inside (l (s (s zero))) ⊃
               (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))
             ∧ ▢ (¬ (var (bvar zero))))))))))))))
  (d-∧-i
   (d-∧-i
    (d-∧-i
     (d-∧-i
      (d-mp
       (d-⊤-i program
        (nd
         (▢-e
          (identity
           (▢ (inside (l (s (s zero))) ∨ after (l (s (s zero)))))))))
       (assume program
        (▢ (inside (l (s (s zero))) ∨ after (l (s (s zero)))))))
      (after-while program (l (s (s (s zero)))) (l (s (s zero)))))
     (d-mp
      (d-⊤-i program
       (nd
        (TL12
         (identity
          (at (l (s (s (s zero)))) ~> after (l (s (s (s zero)))))))))
      (aar program (l (s (s (s zero)))))))
    (wer program (l (s (s zero))) (var (bvar zero))))
   (inside-while program (l (s (s zero)))
    (at (l (s (s zero))) ∨ at (l (s (s (s zero)))))))))