NaturalInduction.agda

ℕ³-induction : ∀ {P : ℕ → ℕ → ℕ → Set} → P 0 0 0 →
               (∀ {n} → P n 0 0 → P (succ n) 0 0) →
               (∀ {m} → P 0 m 0 → P 0 (succ m) 0) →
               (∀ {k} → P 0 0 k → P 0 0 (succ k)) →
               (∀ {n m} → P n m 0 → P (succ n) (succ m) 0) →
               (∀ {n k} → P n 0 k → P (succ n) 0 (succ k)) →
               (∀ {m k} → P 0 m k → P 0 (succ m) (succ k)) →
               (∀ {n m k} → P n m k →
                            P (succ n) m k → P n (succ m) k → P n m (succ k) →
                            P (succ n) (succ m) k → P (succ n) m (succ k) → P n (succ m) (succ k) →
                            P (succ n) (succ m) (succ k)) →
               ∀ n m k → P n m k
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk 0 0 0 = P₀
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk 0 0 (succ k)
  with ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) 0 0 k
...  | ih = Pk ih
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk 0 (succ m) 0
  with ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) 0 m 0
...  | ih = Pm ih
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk (succ n) 0 0
  with ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) n 0 0
...  | ih = Pn ih
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk 0 (succ m) (succ k)
  with ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) 0 m k
...  | ih = Pmk ih
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk (succ n) 0 (succ k)
  with ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) n 0 k
...  | ih = Pnk ih
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk (succ n) (succ m) 0
  with ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) n m 0
...  | ih = Pnm ih
ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk Pnmk (succ n) (succ m) (succ k) = 
  let
      ih-nmk = ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) n        m        k
      ih-k   = ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) n        m        (succ k)
      ih-mk  = ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) n        (succ m) (succ k)
      ih-m   = ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) n        (succ m) k
      ih-nm  = ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) (succ n) (succ m) k
      ih-n   = ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) (succ n) m        k
      ih-nk  = ℕ³-induction P₀ Pn Pm Pk Pnm Pnk Pmk (λ {n m k} → Pnmk {n} {m} {k}) (succ n) m        (succ k)
   in Pnmk ih-nmk ih-n ih-m ih-k ih-nm ih-nk ih-mk