整合的な横棒図

1. 「-----」は、アトミックな証明＝推論ルール
2. 「~~~~~」は、アトミックとは限らない証明（アトミックを排除しない）
3. 「=====」は、アトミックなリーズニング＝タクティク
4. 「+++++」は、アトミックとは限らないリーズニング＝スクリプト

(A∧B)→C ⇒ A→(B→C) のリーズニング

  #1  #2        A∧B    (A∧B)→C
 ---- ----    ----------------------- impl.left_elim
   A   B                 C
  ------- and.intro
     A∧B
 ===================================== Cut 1
  #1  #2
 ---- ----
   A   B 
   ----- and.intro
    A∧B         (A∧B)→C
   ----------------------- impl.left_elim
        C
 ============================ Impl.Intro #2
      #1
      ---
       A   (A∧B)→C
   ~~~~~~~~~~~~~~~~~~
       B→C
 ====================== Impl.Intro #1
      (A∧B)→C
   ~~~~~~~~~~~~~~~~~~
     A→(B→C)

  and.intro: #1[A], #2[B] ⇒ A∧B
  impl.left_elim: A∧B, (A∧B)→C ⇒ C
 ===================================== Cut 1
  #1[A], #2[B], (A∧B)→C ⇒ C
 ============================ Impl.Intro #2
    #1[A], (A∧B)→C ⇒ B→C
 =========================== Impl.Intro #1
    (A∧B)→C ⇒ A→(B→C)

単純に上下逆転。

     (A∧B)→C ⇒ A→(B→C)
 ============================ ↑Impl.Intro #1
    #1[A], (A∧B)→C ⇒ B→C
 ============================ ↑Impl.Intro #2
  #1[A], #2[B], (A∧B)→C ⇒ C
 ===================================== ↑Cut 1
  and.intro: #1[A], #2[B] ⇒ A∧B
  impl.left_elim: A∧B, (A∧B)→C ⇒ C

バックワード・カットをどうするかが問題になる。