{-# OPTIONS --no-termination-check #-}

-- We use Berger's modified bar recursion functional to realize the
-- K-Shift.

module K-Shift-MBR where

open import Logic
open import LogicalFacts
open import Naturals
open import JK-Monads
open import Finite

K-∀-shift-mbr : {R : Ω} {A :   Ω}  
-------------
            (∀(n : )  R  A n)                    -- efqs,
            (∀(n : )  K(A n))  K(∀(n : )  A n)  -- shift.

K-∀-shift-mbr {R} {A} efqs φs p = mbr {0}  ())
  where 
   mbr : {m : }  (∀(i : smaller m)  A(embed i))  R
   mbr {m} s = p(override s  n  efqs n (φs m  x  mbr(append {A} s x)))))