%
% IO uniform proof sequents for INCLL
%

prog : frm -> type.

%
% sqnt is:  G ; D_I \ D_O ; O_I \ O_O --> A
%
sqnt : rctx -> rctx -> rctx -> rctx -> frm -> type.

%
% ie_sqnt1 is: G ; D_I \ D_O ; ( L_I \ L_O ; R_I \ R_O ) --> A >> P
%
ie_sqnt1 : rctx -> rctx -> 
	   rctx -> rctx -> rctx -> rctx -> frm -> atm -> type.

%
% ie_sqnt2 is: G ; D_I \ D_O ; O_I \ ( O_L | O_M | O_R ) --> A >> P
%
ie_sqnt2 : rctx -> rctx -> 
	   rctx -> rctx -> rctx -> rctx -> frm -> atm -> type.

=>_R : sqnt Di Do Oi Oo (A => B)
	 <- (prog A -> sqnt Di Do Oi Oo B).

=0_R : sqnt Di Do Oi Oo (A =0 B)
	<- sqnt (Di ,r # A) (Do ,r del) Oi Oo B.

>=>_R : sqnt Di Do Oi Oo (A >=> B)
	<- r2l Oi Oi'
	<- l2r (# A ,l Oi') Oi''
	<- sqnt Di Do Oi'' Oo'' B
	<- r2l Oo'' (del ,l Oo')
	<- l2r Oo' Oo.

=>>_R : sqnt Di Do Oi Oo (A =>> B)
	<- sqnt Di Do (Oi ,r # A) (Oo ,r del) B.

forall_R : sqnt Di Do Oi Oo (forall Srt Frm)
	<- {x : trm Srt} sqnt Di Do Oi Oo (Frm x).

forall2_R : sqnt Di Do Oi Oo (forall2 Srt1 Srt2 Frm)
	<- {x : trm Srt1 -> trm Srt2} sqnt Di Do Oi Oo (Frm x).

choice_O : sqnt Di Do Oi Oo (^ P)
	<- choose Oi OiL A OiR
	<- ie_sqnt1 Di Do OiL OoL OiR OoR A P
	<- appr (OoL ,r del) OoR Oo.

choice_D : sqnt Di Do Oi Oo (^ P)
	<- choose Di DiL A DiR
	<- appr DiL DiR Di'
	<- ie_sqnt2 Di' Do' Oi Ol Om Or A P
	<- insertAfter DiR (# A) Di' Di	
	<- insertAfter DiR del Do' Do
	<- appr Ol Om Oo'
	<- appr Oo' Or Oo.

choice_G : sqnt Di Do Oi Oo (^ P)
%%%	<- choose G _ A _
        <- prog A 
	<- ie_sqnt2 Di Do Oi Ol Om Or A P
	<- appr Ol Om Oo'
	<- appr Oo' Or Oo.

forall_L1 : {t : trm Srt} ie_sqnt1 Di Do OiL OoL OiR OoR (forall Srt Frm) P
	<- ie_sqnt1 Di Do OiL OoL OiR OoR (Frm t) P.

forall_L2 : {t : trm Srt} ie_sqnt2 Di Do Oi Ol Om Or (forall Srt Frm) P
	<- ie_sqnt2 Di Do Oi Ol Om Or (Frm t) P.

forall2_L1 : {t : trm Srt1 -> trm Srt2} 
	ie_sqnt1 Di Do OiL OoL OiR OoR (forall2 Srt1 Srt2 Frm) P
		<- ie_sqnt1 Di Do OiL OoL OiR OoR (Frm t) P.

forall2_L2 : {t : trm Srt1 -> trm Srt2} 
	ie_sqnt2 Di Do Oi Ol Om Or (forall2 Srt1 Srt2 Frm) P
		<- ie_sqnt2 Di Do Oi Ol Om Or (Frm t) P.


=>_L1 : ie_sqnt1 Di Do OiL OoL OiR OoR (A => B) P
	<- ie_sqnt1 Di Do OiL OoL OiR OoR B P
	<- sqnt rnil rnil rnil rnil A.

=0_L1 : ie_sqnt1 Di Do OiL OoL OiR OoR (A =0 B) P
	<- ie_sqnt1 Di Dm OiL OoL OiR OoR B P
	<- sqnt Dm Do rnil rnil A.

>=>_L1 : ie_sqnt1 Di Do OiL OoL OiR OoR (A >=> B) P
	<- ie_sqnt1 Di Dm OiL OoL' OiR OoR B P
	<- splitr OoL' OoLL OiA
	<- sqnt Dm Do OiA OoA A
	<- appr OoLL OoA OoL.

=>>_L1 : ie_sqnt1 Di Do OiL OoL OiR OoR (A =>> B) P
	<- ie_sqnt1 Di Dm OiL OoL OiR OoR' B P
	<- r2l OoR' OoRl
	<- splitl OoRl OiAl OoRl'
	<- l2r OoRl' OoRL
	<- l2r OiAl OiA
	<- sqnt Dm Do OiA OoA A
	<- appr OoA OoRL OoR.


=>_L2 : ie_sqnt2 Di Do Oi Ol Om Or (A => B) P
	<- ie_sqnt2 Di Do Oi Ol Om Or B P
	<- sqnt rnil rnil rnil rnil A.

=0_L2 : ie_sqnt2 Di Do Oi Ol Om Or (A =0 B) P
	<- ie_sqnt2 Di Dm Oi Ol Om Or B P
	<- sqnt Dm Do rnil rnil A.

>=>_L2 : ie_sqnt2 Di Do Oi Ol OmR Or (A >=> B) P
	<- ie_sqnt2 Di Dm Oi Ol' Om Or B P
	<- sqnt Dm Do Om Om' A
	<- splitr Om' OmL OmR
	<- appr Ol' OmL Ol.

=>>_L2 : ie_sqnt2 Di Do Oi Ol OmL Or (A =>> B) P
	<- ie_sqnt2 Di Dm Oi Ol Om Or' B P
	<- sqnt Dm Do Om Om' A
	<- r2l Om' Om'l
	<- splitl Om'l OmLl OmRl
	<- l2r OmLl OmL
	<- l2r OmRl OmR
	<- appr OmR Or' Or.


init_1 : ie_sqnt1 Di Di OiL OiL OiR OiR (^ P) P.

init_2 : ie_sqnt2 Di Di Oi rnil Oi rnil (^ P) P.