--#include "realisability.agda"

Ex_i2 (A::Set)(P::A -> SP)(x::A)
  :: Realized (Entails (P x) (exists@_ A P))
  = Ex_e A (exists@_ A P) P (idaxiom (exists@_ A P)) x

All_e2 (A::Set)(P::A -> SP)(x::A)
  :: Realized (Entails (forall@_ A P) (P x))
  = All_e A (forall@_ A P) P (idaxiom (forall@_ A P)) x

modus_ponens (a::SP)(b::SP)
  :: Realized (Entails (sand@_ (simp@_ a b) a) b)
  = Imp_e (simp@_ a b) a b (idaxiom (simp@_ a b))

prop_lemma (a::SP)(b::SP)(c::SP)
  :: Realized
       (Entails (simp@_ a (simp@_ b c)) (simp@_ (sand@_ a b) (sand@_ b c)))
  = Imp_i
      (simp@_ a (simp@_ b c))
      (sand@_ a b)
      (sand@_ b c)
      (And_i
         (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
         b
         c
         (cut
            (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
            (sand@_ a b)
            b
            (And_e2 (simp@_ a (simp@_ b c)) (sand@_ a b))
            (And_e2 a b))
         (cut
            (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
            (sand@_ (simp@_ b c) b)
            c
            (And_i
               (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
               (simp@_ b c)
               b
               (cut
                  (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
                  (sand@_ (simp@_ a (simp@_ b c)) a)
                  (simp@_ b c)
                  (And_i
                     (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
                     (simp@_ a (simp@_ b c))
                     a
                     (And_e1 (simp@_ a (simp@_ b c)) (sand@_ a b))
                     (cut
                        (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
                        (sand@_ a b)
                        a
                        (And_e2 (simp@_ a (simp@_ b c)) (sand@_ a b))
                        (And_e1 a b)))
                  (modus_ponens a (simp@_ b c)))
               (cut
                  (sand@_ (simp@_ a (simp@_ b c)) (sand@_ a b))
                  (sand@_ a b)
                  b
                  (And_e2 (simp@_ a (simp@_ b c)) (sand@_ a b))
                  (And_e2 a b)))
            (modus_ponens b c)))

pred_lemma (b::SP)(A::Set)(P::A -> SP)
  :: Realized
       (Entails
          (forall@_ A (\(x::A) -> simp@_ (P x) b))
          (simp@_ (exists@_ A P) b))
  = Imp_i
      (forall@_ A (\(x::A) -> simp@_ (P x) b))
      (exists@_ A P)
      b
      (cut
         (sand@_ (forall@_ A (\(x::A) -> simp@_ (P x) b)) (exists@_ A P))
         (sand@_ (exists@_ A P) (forall@_ A (\(x::A) -> simp@_ (P x) b)))
         b
         (And_i
            (sand@_ (forall@_ A (\(x::A) -> simp@_ (P x) b)) (exists@_ A P))
            (exists@_ A P)
            (forall@_ A (\(x::A) -> simp@_ (P x) b))
            (And_e2 (forall@_ A (\(x::A) -> simp@_ (P x) b)) (exists@_ A P))
            (And_e1 (forall@_ A (\(x::A) -> simp@_ (P x) b)) (exists@_ A P)))
         (Imp_e
            (exists@_ A P)
            (forall@_ A (\(x::A) -> simp@_ (P x) b))
            b
            (Ex_i
               A
               (simp@_ (forall@_ A (\(x::A) -> simp@_ (P x) b)) b)
               P
               (\(x::A) ->
                Imp_i
                  (P x)
                  (forall@_ A (\(x'::A) -> simp@_ (P x') b))
                  b
                  (cut
                     (sand@_ (P x) (forall@_ A (\(x'::A) -> simp@_ (P x') b)))
                     (sand@_ (simp@_ (P x) b) (P x))
                     b
                     (And_i
                        (sand@_ (P x) (forall@_ A (\(x'::A) -> simp@_ (P x') b)))
                        (simp@_ (P x) b)
                        (P x)
                        (cut
                           (sand@_
                              (P x)
                              (forall@_ A (\(x'::A) -> simp@_ (P x') b)))
                           (forall@_ A (\(x'::A) -> simp@_ (P x') b))
                           (simp@_ (P x) b)
                           (And_e2
                              (P x)
                              (forall@_ A (\(x'::A) -> simp@_ (P x') b)))
                           (All_e2 A (\(x'::A) -> simp@_ (P x') b) x))
                        (And_e1 (P x) (forall@_ A (\(x'::A) -> simp@_ (P x') b))))
                     (modus_ponens (P x) b))))))

(+) (m::Nat)(n::Nat) :: Nat
  = case n of {
      (zero) -> m;
      (succ x) -> succ@_ (m + x);}

ind (P::Nat -> SP)
  :: Realized
       (Entails
          (sand@_
             (P zero@_)
             (forall@_ Nat (\(n::Nat) -> simp@_ (P n) (P (succ@_ n)))))
          (forall@_ Nat (\(n::Nat) -> P n)))
  = struct {
      real =
        \(h::Cr
               (sand@_
                  (P zero@_)
                  (forall@_ Nat (\(n::Nat) -> simp@_ (P n) (P (succ@_ n)))))) ->
        \(x::Nat) ->
        rec
          (\(z::Nat) -> Cr (P z))
          x
          h._1
          (\(x'::Nat) -> \(y::Cr (P x')) -> h._2 x' y);
      pf =
        struct {
          _1 =
            \(h::Cr
                   (sand@_
                      (P zero@_)
                      (forall@_ Nat (\(n::Nat) -> simp@_ (P n) (P (succ@_ n)))))) ->
            \(r::MR
                   (sand@_
                      (P zero@_)
                      (forall@_ Nat (\(n::Nat) -> simp@_ (P n) (P (succ@_ n)))))
                   h) ->
            \(n::Nat) ->
            rec
              (\(z::Nat) -> MR (P z) (real h z))
              n
              r._1
              (\(x::Nat) ->
               \(y::MR (P x) (real h x)) ->
               let p2 :: MR (simp@_ (P x) (P (succ@_ x))) (h._2 x)
                     = r._2 x
               in  p2._1
                     (rec
                        (\(z::Nat) -> Cr (P z))
                        x
                        h._1
                        (\(x'::Nat) -> \(y'::Cr (P x')) -> h._2 x' y'))
                     y);
          _2 =
            \(h::Tp
                   (sand@_
                      (P zero@_)
                      (forall@_ Nat (\(n::Nat) -> simp@_ (P n) (P (succ@_ n)))))) ->
            \(x::Nat) ->
            rec
              (\(z::Nat) -> Tp (P z))
              x
              h._1
              (\(x'::Nat) -> \(y::Tp (P x')) -> h._2 x' y);};}

postulate G :: Nat -> Nat -> Set

Ax1 :: SP
  = atom@_ (G zero@_ zero@_)

Ax2 :: SP
  = atom@_ (G (succ@_ zero@_) (succ@_ zero@_))

Ax3 :: SP
  = forall@_
      Nat
      (\(n::Nat) ->
       forall@_
         Nat
         (\(k::Nat) ->
          forall@_
            Nat
            (\(l::Nat) ->
             simp@_
               (atom@_ (G n k))
               (simp@_
                  (atom@_ (G (succ@_ n) l))
                  (atom@_ (G (succ@_ (succ@_ n)) (k + l)))))))

Q (n::Nat)(k::Nat)(l::Nat) :: SP
  = sand@_ (atom@_ (G n k)) (atom@_ (G (succ@_ n) l))

F (n::Nat) :: SP
  = exists@_ Nat (\(k::Nat) -> exists@_ Nat (\(l::Nat) -> Q n k l))

fib_lm (x::Nat)
  :: Realized (Entails Ax3 (simp@_ (F x) (F (succ@_ x))))
  = cut
      Ax3
      (forall@_
         Nat
         (\(k::Nat) ->
          forall@_ Nat (\(l::Nat) -> simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))))
      (simp@_ (F x) (F (succ@_ x)))
      (cut
         Ax3
         (forall@_
            Nat
            (\(k::Nat) ->
             forall@_
               Nat
               (\(l::Nat) ->
                simp@_
                  (atom@_ (G x k))
                  (simp@_
                     (atom@_ (G (succ@_ x) l))
                     (atom@_ (G (succ@_ (succ@_ x)) (k + l)))))))
         (forall@_
            Nat
            (\(k::Nat) ->
             forall@_
               Nat
               (\(l::Nat) -> simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))))
         (All_e2
            Nat
            (\(n::Nat) ->
             forall@_
               Nat
               (\(k::Nat) ->
                forall@_
                  Nat
                  (\(l::Nat) ->
                   simp@_
                     (atom@_ (G n k))
                     (simp@_
                        (atom@_ (G (succ@_ n) l))
                        (atom@_ (G (succ@_ (succ@_ n)) (k + l)))))))
            x)
         (All_i
            Nat
            (forall@_
               Nat
               (\(k::Nat) ->
                forall@_
                  Nat
                  (\(l::Nat) ->
                   simp@_
                     (atom@_ (G x k))
                     (simp@_
                        (atom@_ (G (succ@_ x) l))
                        (atom@_ (G (succ@_ (succ@_ x)) (k + l)))))))
            (\(k::Nat) ->
             forall@_
               Nat
               (\(l::Nat) -> simp@_ (Q x k l) (Q (succ@_ x) l (k + l))))
            (\(k::Nat) ->
             All_i
               Nat
               (forall@_
                  Nat
                  (\(k'::Nat) ->
                   forall@_
                     Nat
                     (\(l::Nat) ->
                      simp@_
                        (atom@_ (G x k'))
                        (simp@_
                           (atom@_ (G (succ@_ x) l))
                           (atom@_ (G (succ@_ (succ@_ x)) (k' + l)))))))
               (\(l::Nat) -> simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))
               (\(l::Nat) ->
                cut
                  (forall@_
                     Nat
                     (\(k'::Nat) ->
                      forall@_
                        Nat
                        (\(l'::Nat) ->
                         simp@_
                           (atom@_ (G x k'))
                           (simp@_
                              (atom@_ (G (succ@_ x) l'))
                              (atom@_ (G (succ@_ (succ@_ x)) (k' + l')))))))
                  (forall@_
                     Nat
                     (\(l'::Nat) ->
                      simp@_
                        (atom@_ (G x k))
                        (simp@_
                           (atom@_ (G (succ@_ x) l'))
                           (atom@_ (G (succ@_ (succ@_ x)) (k + l'))))))
                  (simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))
                  (All_e2
                     Nat
                     (\(k'::Nat) ->
                      forall@_
                        Nat
                        (\(l'::Nat) ->
                         simp@_
                           (atom@_ (G x k'))
                           (simp@_
                              (atom@_ (G (succ@_ x) l'))
                              (atom@_ (G (succ@_ (succ@_ x)) (k' + l'))))))
                     k)
                  (cut
                     (forall@_
                        Nat
                        (\(l'::Nat) ->
                         simp@_
                           (atom@_ (G x k))
                           (simp@_
                              (atom@_ (G (succ@_ x) l'))
                              (atom@_ (G (succ@_ (succ@_ x)) (k + l'))))))
                     (simp@_
                        (atom@_ (G x k))
                        (simp@_
                           (atom@_ (G (succ@_ x) l))
                           (atom@_ (G (succ@_ (succ@_ x)) (k + l)))))
                     (simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))
                     (All_e2
                        Nat
                        (\(l'::Nat) ->
                         simp@_
                           (atom@_ (G x k))
                           (simp@_
                              (atom@_ (G (succ@_ x) l'))
                              (atom@_ (G (succ@_ (succ@_ x)) (k + l')))))
                        l)
                     (prop_lemma
                        (atom@_ (G x k))
                        (atom@_ (G (succ@_ x) l))
                        (atom@_ (G (succ@_ (succ@_ x)) (k + l)))))))))
      (cut
         (forall@_
            Nat
            (\(k::Nat) ->
             forall@_
               Nat
               (\(l::Nat) -> simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))))
         (forall@_
            Nat
            (\(x'::Nat) ->
             simp@_ (exists@_ Nat (\(l::Nat) -> Q x x' l)) (F (succ@_ x))))
         (simp@_ (F x) (F (succ@_ x)))
         (All_i
            Nat
            (forall@_
               Nat
               (\(k::Nat) ->
                forall@_
                  Nat
                  (\(l::Nat) -> simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))))
            (\(x'::Nat) ->
             simp@_ (exists@_ Nat (\(l::Nat) -> Q x x' l)) (F (succ@_ x)))
            (\(k::Nat) ->
             cut
               (forall@_
                  Nat
                  (\(k'::Nat) ->
                   forall@_
                     Nat
                     (\(l::Nat) -> simp@_ (Q x k' l) (Q (succ@_ x) l (k' + l)))))
               (forall@_ Nat (\(x'::Nat) -> simp@_ (Q x k x') (F (succ@_ x))))
               (simp@_ (exists@_ Nat (\(l::Nat) -> Q x k l)) (F (succ@_ x)))
               (All_i
                  Nat
                  (forall@_
                     Nat
                     (\(k'::Nat) ->
                      forall@_
                        Nat
                        (\(l::Nat) ->
                         simp@_ (Q x k' l) (Q (succ@_ x) l (k' + l)))))
                  (\(x'::Nat) -> simp@_ (Q x k x') (F (succ@_ x)))
                  (\(l::Nat) ->
                   cut
                     (forall@_
                        Nat
                        (\(k'::Nat) ->
                         forall@_
                           Nat
                           (\(l'::Nat) ->
                            simp@_ (Q x k' l') (Q (succ@_ x) l' (k' + l')))))
                     (forall@_
                        Nat
                        (\(l'::Nat) ->
                         simp@_ (Q x k l') (Q (succ@_ x) l' (k + l'))))
                     (simp@_ (Q x k l) (F (succ@_ x)))
                     (All_e2
                        Nat
                        (\(k'::Nat) ->
                         forall@_
                           Nat
                           (\(l'::Nat) ->
                            simp@_ (Q x k' l') (Q (succ@_ x) l' (k' + l'))))
                        k)
                     (cut
                        (forall@_
                           Nat
                           (\(l'::Nat) ->
                            simp@_ (Q x k l') (Q (succ@_ x) l' (k + l'))))
                        (simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))
                        (simp@_ (Q x k l) (F (succ@_ x)))
                        (All_e2
                           Nat
                           (\(l'::Nat) ->
                            simp@_ (Q x k l') (Q (succ@_ x) l' (k + l')))
                           l)
                        (Imp_i
                           (simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))
                           (Q x k l)
                           (F (succ@_ x))
                           (cut
                              (sand@_
                                 (simp@_ (Q x k l) (Q (succ@_ x) l (k + l)))
                                 (Q x k l))
                              (Q (succ@_ x) l (k + l))
                              (F (succ@_ x))
                              (modus_ponens (Q x k l) (Q (succ@_ x) l (k + l)))
                              (cut
                                 (Q (succ@_ x) l (k + l))
                                 (exists@_ Nat (\(l'::Nat) -> Q (succ@_ x) l l'))
                                 (F (succ@_ x))
                                 (Ex_i2
                                    Nat
                                    (\(l'::Nat) -> Q (succ@_ x) l l')
                                    (k + l))
                                 (Ex_i2
                                    Nat
                                    (\(k'::Nat) ->
                                     exists@_
                                       Nat
                                       (\(l'::Nat) -> Q (succ@_ x) k' l'))
                                    l)))))))
               (pred_lemma (F (succ@_ x)) Nat (\(l::Nat) -> Q x k l))))
         (pred_lemma
            (F (succ@_ x))
            Nat
            (\(k::Nat) -> exists@_ Nat (\(l::Nat) -> Q x k l))))

fib_thm
  :: Realized
       (Entails
          (sand@_ (sand@_ Ax1 Ax2) Ax3)
          (forall@_ Nat (\(n::Nat) -> F n)))
  = cut
      (sand@_ (sand@_ Ax1 Ax2) Ax3)
      (sand@_
         (F zero@_)
         (forall@_ Nat (\(n::Nat) -> simp@_ (F n) (F (succ@_ n)))))
      (forall@_ Nat (\(n::Nat) -> F n))
      (And_i
         (sand@_ (sand@_ Ax1 Ax2) Ax3)
         (F zero@_)
         (forall@_ Nat (\(n::Nat) -> simp@_ (F n) (F (succ@_ n))))
         (cut
            (sand@_ (sand@_ Ax1 Ax2) Ax3)
            (sand@_ Ax1 Ax2)
            (F zero@_)
            (And_e1 (sand@_ Ax1 Ax2) Ax3)
            (cut
               (sand@_ Ax1 Ax2)
               (exists@_ Nat (\(l::Nat) -> Q zero@_ zero@_ l))
               (F zero@_)
               (Ex_i2 Nat (\(l::Nat) -> Q zero@_ zero@_ l) (succ@_ zero@_))
               (Ex_i2
                  Nat
                  (\(k::Nat) -> exists@_ Nat (\(l::Nat) -> Q zero@_ k l))
                  zero@_)))
         (cut
            (sand@_ (sand@_ Ax1 Ax2) Ax3)
            Ax3
            (forall@_ Nat (\(n::Nat) -> simp@_ (F n) (F (succ@_ n))))
            (And_e2 (sand@_ Ax1 Ax2) Ax3)
            (All_i
               Nat
               Ax3
               (\(n::Nat) -> simp@_ (F n) (F (succ@_ n)))
               (\(x::Nat) -> fib_lm x))))
      (ind F)


nocontent :: Cr (sand@_ (sand@_ Ax1 Ax2) Ax3)
  = struct {
      _1 =
        struct {
          _1 = elt@_;
          _2 = elt@_;};
      _2 =
        \(x::Nat) ->
        \(x'::Nat) ->
        \(x0::Nat) ->
        \(h::Cr (atom@_ (G x x'))) ->
        \(h'::Cr (atom@_ (G (succ@_ x) x0))) ->
        elt@_;}


fib_prog (x::Nat) :: Nat
  = (fib_thm.real nocontent x)._1




{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
 #-}