Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/7cc032fed95098bdf3096efbbe30d268]
prop : type.
top : prop.
imp : prop -> prop -> prop.
and : prop -> prop -> prop.
hyp : prop -> type.
conc : prop -> type.
init : {A:prop} hyp A -> conc A.
topR : conc top.
andL :
   {A:prop} {B:prop} {C:prop}
      (hyp A -> hyp B -> conc C) -> hyp (and A B) -> conc C.
andR : {A:prop} {B:prop} conc A -> conc B -> conc (and A B).
impL :
   {A:prop} {B:prop} {C:prop}
      conc A -> (hyp B -> conc C) -> hyp (imp A B) -> conc C.
impR : {A:prop} {B:prop} (hyp A -> conc B) -> conc (imp A B).
cut : {C:prop} {A:prop} conc A -> (hyp A -> conc C) -> conc C -> type.
%mode +{C:prop} +{A:prop} +{D:conc A} +{E:hyp A -> conc C} -{F:conc C} (cut A D E F).
initD :
   {A1:prop} {A:prop} {Ha:hyp A} {E:hyp A -> conc A1}
      cut A (init Ha) ([Ha1:hyp A] E Ha1) (E Ha).
initE : {A:prop} {D:conc A} cut A D ([Ha:hyp A] init Ha) D.
closed : {A1:prop} {A:prop} {D:conc A} {E':conc A1} cut A D ([Ha:hyp A] E') E'.
andC :
   {A1:prop} {B:prop} {D2:conc B} {F2:hyp B -> conc A1} {F:conc A1} {A:prop}
      {D1:conc A} {F1:hyp A -> hyp B -> conc A1}
      {E':hyp (and A B) -> hyp A -> hyp B -> conc A1}
      cut B D2 ([Hb:hyp B] F2 Hb) F
         -> ({Hb:hyp B} cut A D1 ([Ha:hyp A] F1 Ha Hb) (F2 Hb))
         -> ({Ha:hyp A} {Hb:hyp B}
                cut (and A B) (andR D1 D2) ([Hab:hyp (and A B)] E' Hab Ha Hb)
                   (F1 Ha Hb))
         -> cut (and A B) (andR D1 D2)
               ([Hab:hyp (and A B)]
                   andL ([Ha:hyp A] [Hb:hyp B] E' Hab Ha Hb) Hab) F.
impC :
   {C:prop} {B:prop} {F3:conc B} {F2:hyp B -> conc C} {F:conc C} {A:prop}
      {F1:conc A} {D':hyp A -> conc B} {E2:hyp (imp A B) -> hyp B -> conc C}
      {E1:hyp (imp A B) -> conc A}
      cut B F3 ([x:hyp B] F2 x) F -> cut A F1 ([x:hyp A] D' x) F3
         -> ({Hb:hyp B}
                cut (imp A B) (impR ([x:hyp A] D' x))
                   ([Hab:hyp (imp A B)] E2 Hab Hb) (F2 Hb))
         -> cut (imp A B) (impR ([x:hyp A] D' x)) ([x:hyp (imp A B)] E1 x) F1
         -> cut (imp A B) (impR ([Ha:hyp A] D' Ha))
               ([Hab:hyp (imp A B)] impL (E1 Hab) ([Hb:hyp B] E2 Hab Hb) Hab) F.
andLLC :
   {A1:prop} {A2:prop} {A3:prop} {A:prop} {D':hyp A1 -> hyp A2 -> conc A}
      {E:hyp A -> conc A3} {F':hyp A1 -> hyp A2 -> conc A3}
      {Hab:hyp (and A1 A2)}
      ({Ha:hyp A1} {Hb:hyp A2} cut A (D' Ha Hb) ([x:hyp A] E x) (F' Ha Hb))
         -> cut A (andL ([Ha:hyp A1] [Hb:hyp A2] D' Ha Hb) Hab) ([x:hyp A] E x)
               (andL ([Ha:hyp A1] [Hb:hyp A2] F' Ha Hb) Hab).
impLLC :
   {A1:prop} {A2:prop} {A:prop} {D2:hyp A1 -> conc A} {E:hyp A -> conc A2}
      {F2:hyp A1 -> conc A2} {A3:prop} {D1:conc A3} {Hi:hyp (imp A3 A1)}
      ({Hb:hyp A1} cut A (D2 Hb) ([x:hyp A] E x) (F2 Hb))
         -> cut A (impL D1 ([Hb:hyp A1] D2 Hb) Hi) ([x:hyp A] E x)
               (impL D1 ([x:hyp A1] F2 x) Hi).
andRRC :
   {A1:prop} {A:prop} {D:conc A} {E2:hyp A -> conc A1} {F2:conc A1} {A2:prop}
      {E1:hyp A -> conc A2} {F1:conc A2}
      cut A D ([x:hyp A] E2 x) F2 -> cut A D ([x:hyp A] E1 x) F1
         -> cut A D ([Ha:hyp A] andR (E1 Ha) (E2 Ha)) (andR F1 F2).
impRRC :
   {A1:prop} {A2:prop} {A:prop} {D:conc A} {E1:hyp A -> hyp A1 -> conc A2}
      {F1:hyp A1 -> conc A2}
      ({H1:hyp A1} cut A D ([Ha:hyp A] E1 Ha H1) (F1 H1))
         -> cut A D ([Ha:hyp A] impR ([H1:hyp A1] E1 Ha H1))
               (impR ([H1:hyp A1] F1 H1)).
andLRC :
   {A1:prop} {A2:prop} {A3:prop} {A:prop} {D:conc A}
      {E':hyp A -> hyp A1 -> hyp A2 -> conc A3} {F':hyp A1 -> hyp A2 -> conc A3}
      {Hp:hyp (and A1 A2)}
      ({H1:hyp A1} {H2:hyp A2} cut A D ([Ha:hyp A] E' Ha H1 H2) (F' H1 H2))
         -> cut A D ([Ha:hyp A] andL ([H1:hyp A1] [H2:hyp A2] E' Ha H1 H2) Hp)
               (andL ([H1:hyp A1] [H2:hyp A2] F' H1 H2) Hp).
impLRC :
   {A1:prop} {A2:prop} {A:prop} {D:conc A} {E2:hyp A -> hyp A1 -> conc A2}
      {F2:hyp A1 -> conc A2} {A3:prop} {E1:hyp A -> conc A3} {F1:conc A3}
      {Hi:hyp (imp A3 A1)}
      ({Hb:hyp A1} cut A D ([Ha:hyp A] E2 Ha Hb) (F2 Hb))
         -> cut A D ([Ha:hyp A] E1 Ha) F1
         -> cut A D ([Ha:hyp A] impL (E1 Ha) ([Hb:hyp A1] E2 Ha Hb) Hi)
               (impL F1 ([Hb:hyp A1] F2 Hb) Hi).
%block hyp : some {A:prop} block {H:hyp A}.
%worlds (hyp) (cut _ _ _ _).
%total {A [D E]} (cut A D E F).
[Closing file /home/www/twelfwiki/code/7cc032fed95098bdf3096efbbe30d268]
%% OK %%