Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/fe368384cabeda311b02f11adbf98452]
tp : type.
unit : tp.
arrow : tp -> tp -> tp.
tm : type.
empty : tm.
lam : tp -> (tm -> tm) -> tm.
app : tm -> tm -> tm.
nat : type.
z : nat.
s : nat -> nat.
plus : nat -> nat -> nat -> type.
%mode +{X1:nat} +{X2:nat} -{X3:nat} (plus X1 X2 X3).
plus-z : {N2:nat} plus z N2 N2.
plus-s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
%worlds () (plus _ _ _).
%total N (plus N _ _).
plus-exists : {N3:nat} {N1:nat} {N2:nat} plus N1 N2 N3 -> type.
%mode -{N3:nat} +{X1:nat} +{X2:nat} -{X3:plus X1 X2 N3} (plus-exists X1 X2 X3).
- : {X1:nat} plus-exists z X1 plus-z.
- :
   {X1:nat} {N1:nat} {N2:nat} {D:plus N1 N2 X1}
      plus-exists N1 N2 D -> plus-exists (s N1) N2 (plus-s D).
%worlds () (plus-exists _ _ _).
%total N1 (plus-exists N1 _ _).
plus-z-rh : {n:nat} plus n z n -> type.
%mode +{N:nat} -{D:plus N z N} (plus-z-rh N D).
- : plus-z-rh z plus-z.
- : {N:nat} {D:plus N z N} plus-z-rh N D -> plus-z-rh (s N) (plus-s D).
%worlds () (plus-z-rh _ _).
%total N (plus-z-rh N _).
plus-s-rh :
   {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:plus N1 N2 N3} -{D2:plus N1 (s N2) (s N3)}
   (plus-s-rh D1 D2).
- : {X1:nat} plus-s-rh plus-z plus-z.
- :
   {N1':nat} {N2:nat} {N3':nat} {D:plus N1' N2 N3'} {D':plus N1' (s N2) (s N3')}
      plus-s-rh D D' -> plus-s-rh (plus-s D) (plus-s D').
%worlds () (plus-s-rh _ _).
%total D (plus-s-rh D _).
plus-commute :
   {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus N2 N1 N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:plus N1 N2 N3} -{D2:plus N2 N1 N3}
   (plus-commute D1 D2).
- : {N:nat} {D:plus N z N} plus-z-rh N D -> plus-commute plus-z D.
- :
   {N2:nat} {N1:nat} {N3:nat} {D':plus N2 N1 N3} {D'':plus N2 (s N1) (s N3)}
      {D:plus N1 N2 N3}
      plus-s-rh D' D'' -> plus-commute D D' -> plus-commute (plus-s D) D''.
%worlds () (plus-commute _ _).
%total D (plus-commute D _).
id/nat : nat -> nat -> type.
id/nat-refl : {N:nat} id/nat N N.
id/nat-s-cong : {N1:nat} {N2:nat} id/nat N1 N2 -> id/nat (s N1) (s N2) -> type.
%mode +{N1:nat} +{N2:nat} +{X1:id/nat N1 N2} -{X2:id/nat (s N1) (s N2)}
   (id/nat-s-cong X1 X2).
- : {X1:nat} id/nat-s-cong id/nat-refl id/nat-refl.
%worlds () (id/nat-s-cong _ _).
%total {} (id/nat-s-cong _ _).
plus-unique :
   {N1:nat} {N2:nat} {N3:nat} {N3':nat}
      plus N1 N2 N3 -> plus N1 N2 N3' -> id/nat N3 N3' -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{N3':nat} +{X1:plus N1 N2 N3}
   +{X2:plus N1 N2 N3'} -{X3:id/nat N3 N3'} (plus-unique X1 X2 X3).
- : {X1:nat} {X2:nat} {X3:nat} {D:plus X1 X2 X3} plus-unique D D id/nat-refl.
- :
   {X1:nat} {X2:nat} {Did:id/nat X1 X2} {DidS:id/nat (s X1) (s X2)} {X3:nat}
      {X4:nat} {D:plus X3 X4 X1} {D':plus X3 X4 X2}
      id/nat-s-cong Did DidS -> plus-unique D D' Did
         -> plus-unique (plus-s D) (plus-s D') DidS.
%worlds () (plus-unique _ _ _).
%total D (plus-unique D _ _).
plus-respects-id :
   {N1:nat} {N2:nat} {N3:nat} {N1':nat} {N2':nat} {N3':nat}
      plus N1 N2 N3 -> id/nat N1 N1' -> id/nat N2 N2' -> id/nat N3 N3'
         -> plus N1' N2' N3' -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{N1':nat} +{N2':nat} +{N3':nat}
   +{X1:plus N1 N2 N3} +{X2:id/nat N1 N1'} +{X3:id/nat N2 N2'}
   +{X4:id/nat N3 N3'} -{X5:plus N1' N2' N3'} (plus-respects-id X1 X2 X3 X4 X5).
- :
   {X1:nat} {X2:nat} {X3:nat} {D:plus X1 X2 X3}
      plus-respects-id D id/nat-refl id/nat-refl id/nat-refl D.
%worlds () (plus-respects-id _ _ _ _ _).
%total {} (plus-respects-id _ _ _ _ _).
id/nat-sym : {N1:nat} {N2:nat} id/nat N1 N2 -> id/nat N2 N1 -> type.
%mode +{N1:nat} +{N2:nat} +{X1:id/nat N1 N2} -{X2:id/nat N2 N1} (id/nat-sym X1 X2).
- : {X1:nat} id/nat-sym id/nat-refl id/nat-refl.
%worlds () (id/nat-sym _ _).
%total {} (id/nat-sym _ _).
plus-assoc :
   {A:nat} {B:nat} {AB:nat} {C:nat} {BC:nat} {ABC:nat}
      plus A B AB -> plus B C BC -> plus AB C ABC -> plus A BC ABC -> type.
%mode +{A:nat} +{B:nat} +{AB:nat} +{C:nat} +{BC:nat} +{ABC:nat} +{X1:plus A B AB}
   +{X2:plus B C BC} +{X3:plus AB C ABC} -{X4:plus A BC ABC}
   (plus-assoc X1 X2 X3 X4).
- :
   {X1:nat} {X2:nat} {Did:id/nat X1 X2} {Dplus:plus z X1 X2} {X3:nat} {X4:nat}
      {DplusB-C:plus X3 X4 X1} {DplusB-C':plus X3 X4 X2}
      plus-respects-id plus-z id/nat-refl id/nat-refl Did Dplus
         -> plus-unique DplusB-C DplusB-C' Did
         -> plus-assoc plus-z DplusB-C DplusB-C' Dplus.
- :
   {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat}
      {DplusA'-B:plus X1 X2 X3} {DplusB-C:plus X2 X4 X5}
      {DplusA'B-C:plus X3 X4 X6} {DplusA'-BC:plus X1 X5 X6}
      plus-assoc DplusA'-B DplusB-C DplusA'B-C DplusA'-BC
         -> plus-assoc (plus-s DplusA'-B) DplusB-C (plus-s DplusA'B-C)
               (plus-s DplusA'-BC).
%worlds () (plus-assoc _ _ _ _).
%total D (plus-assoc D _ _ _).
plus-assoc2 :
   {A:nat} {B:nat} {AB:nat} {C:nat} {BC:nat} {ABC:nat}
      plus A B AB -> plus B C BC -> plus AB C ABC -> plus A BC ABC -> type.
%mode +{A:nat} +{B:nat} +{AB:nat} +{C:nat} +{BC:nat} +{ABC:nat} +{X1:plus A B AB}
   +{X2:plus B C BC} -{X3:plus AB C ABC} +{X4:plus A BC ABC}
   (plus-assoc2 X1 X2 X3 X4).
- :
   {X1:nat} {X2:nat} {X3:nat} {X4:nat} {D3:plus X1 X2 X3} {Did':id/nat X3 X4}
      {D3':plus X1 X2 X4} {Did:id/nat X4 X3} {X5:nat} {X6:nat}
      {D4:plus X5 X6 X4} {D4':plus X5 X6 X3} {X7:nat} {D1:plus X5 X7 X1}
      {D2:plus X7 X2 X6}
      plus-respects-id D3 id/nat-refl id/nat-refl Did' D3'
         -> id/nat-sym Did Did' -> plus-unique D4 D4' Did
         -> plus-assoc D1 D2 D3 D4' -> plus-exists X1 X2 D3
         -> plus-assoc2 D1 D2 D3' D4.
%worlds () (plus-assoc2 _ _ _ _).
%total {} (plus-assoc2 _ _ _ _).
lemma :
   {N1:nat} {N2:nat} {Nsum:nat} {Ndiff1:nat} {N1':nat} {Ndiff2:nat} {N2':nat}
      {Nsum':nat} {Ndiff:nat}
      plus N1 N2 Nsum -> plus Ndiff1 N1 N1' -> plus Ndiff2 N2 N2'
         -> plus N1' N2' Nsum' -> plus Ndiff Nsum Nsum' -> type.
%mode +{N1:nat} +{N2:nat} +{Nsum:nat} +{Ndiff1:nat} +{N1':nat} +{Ndiff2:nat}
   +{N2':nat} +{Nsum':nat} -{Ndiff:nat} +{X1:plus N1 N2 Nsum}
   +{X2:plus Ndiff1 N1 N1'} +{X3:plus Ndiff2 N2 N2'} +{X4:plus N1' N2' Nsum'}
   -{X5:plus Ndiff Nsum Nsum'} (lemma X1 X2 X3 X4 X5).
- :
   {Nsum:nat} {Ndiff1+2:nat} {Nsum':nat} {Dres:plus Nsum Ndiff1+2 Nsum'}
      {Dres':plus Ndiff1+2 Nsum Nsum'} {N1:nat} {N2:nat} {Ndiff1+2':nat}
      {D:plus N1 N2 Nsum} {Dassoc'':plus N2 Ndiff1+2 Ndiff1+2'}
      {Dassoc:plus N1 Ndiff1+2' Nsum'} {Dassoc':plus Ndiff1+2 N2 Ndiff1+2'}
      {Ndiff1:nat} {Ndiff2:nat} {N2':nat} {Ddiff1+2:plus Ndiff1 Ndiff2 Ndiff1+2}
      {D2':plus Ndiff2 N2 N2'} {Ddiff1+2':plus Ndiff1 N2' Ndiff1+2'}
      {D2:plus N2 Ndiff2 N2'} {N1':nat} {D1:plus N1 Ndiff1 N1'}
      {D':plus N1' N2' Nsum'} {D2pre:plus Ndiff2 N2 N2'}
      {D1pre:plus Ndiff1 N1 N1'}
      plus-commute Dres Dres' -> plus-assoc2 D Dassoc'' Dres Dassoc
         -> plus-commute Dassoc' Dassoc''
         -> plus-assoc2 Ddiff1+2 D2' Dassoc' Ddiff1+2'
         -> plus-exists Ndiff1 Ndiff2 Ddiff1+2 -> plus-commute D2 D2'
         -> plus-assoc D1 Ddiff1+2' D' Dassoc
         -> plus-exists Ndiff1 N2' Ddiff1+2' -> plus-commute D2pre D2
         -> plus-commute D1pre D1 -> lemma D D1pre D2pre D' Dres'.
%worlds () (lemma _ _ _ _ _).
%total {} (lemma _ _ _ _ _).
size : tm -> nat -> type.
%mode +{E:tm} -{N:nat} (size E N).
size-empty : size empty (s z).
size-lam :
   {E:tm -> tm} {N:nat} {X1:tp}
      ({x:tm} size x (s z) -> size (E x) N) -> size (lam X1 ([x:tm] E x)) (s N).
size-app :
   {N1:nat} {N2:nat} {N:nat} {E2:tm} {E1:tm}
      plus N1 N2 N -> size E2 N2 -> size E1 N1 -> size (app E1 E2) (s N).
%block size-block : block {x:tm} {dx:size x (s z)}.
%worlds (size-block) (size _ _).
%total E (size E _).
subst-size :
   {E:tm -> tm} {N:nat} {N':nat} {Ndiff:nat} {E':tm}
      ({x:tm} size x (s z) -> size (E x) N) -> size (E E') N' -> plus Ndiff N N'
         -> type.
%mode +{E:tm -> tm} +{N:nat} +{N':nat} -{Ndiff:nat} +{E':tm}
   +{D1:{x:tm} size x (s z) -> size (E x) N} +{D2:size (E E') N'}
   -{DL:plus Ndiff N N'} (subst-size E' D1 D2 DL).
%worlds (size-block) (subst-size _ _ _ _).
plus-s-rh :
   {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:plus N1 N2 N3} -{D2:plus N1 (s N2) (s N3)}
   (plus-s-rh D1 D2).
%worlds () (plus-s-rh _ _).
plus-commute :
   {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus N2 N1 N3 -> type.
%mode +{N1:nat} +{N2:nat} +{N3:nat} +{D1:plus N1 N2 N3} -{D2:plus N2 N1 N3}
   (plus-commute D1 D2).
%worlds () (plus-commute _ _).
lemma :
   {N1:nat} {N2:nat} {Nsum:nat} {Ndiff1:nat} {N1':nat} {Ndiff2:nat} {N2':nat}
      {Nsum':nat} {Ndiff:nat}
      plus N1 N2 Nsum -> plus Ndiff1 N1 N1' -> plus Ndiff2 N2 N2'
         -> plus N1' N2' Nsum' -> plus Ndiff Nsum Nsum' -> type.
%mode +{N1:nat} +{N2:nat} +{Nsum:nat} +{Ndiff1:nat} +{N1':nat} +{Ndiff2:nat}
   +{N2':nat} +{Nsum':nat} -{Ndiff:nat} +{X1:plus N1 N2 Nsum}
   +{X2:plus Ndiff1 N1 N1'} +{X3:plus Ndiff2 N2 N2'} +{X4:plus N1' N2' Nsum'}
   -{X5:plus Ndiff Nsum Nsum'} (lemma X1 X2 X3 X4 X5).
%worlds () (lemma _ _ _ _ _).
size-at-least-one : {E:tm} {N:nat} {N':nat} size E N -> plus (s z) N' N -> type.
%mode +{E:tm} +{N:nat} -{N':nat} +{X1:size E N} -{X2:plus (s z) N' N}
   (size-at-least-one X1 X2).
- : {X1:tm} {X2:nat} {X3:size X1 (s X2)} size-at-least-one X3 (plus-s plus-z).
%worlds (size-block) (size-at-least-one _ _).
%total {} (size-at-least-one _ _).
[Closing file /home/www/twelfwiki/code/fe368384cabeda311b02f11adbf98452]
%% OK %%