graph_pair[T: TYPE]: THEORY
BEGIN

  i,j,k,l,m,n,h,g: VAR nat

  lsth(p1:[nat,nat], p2:[nat,nat]): bool = LET (i,j) = p1, (k,l) = p2 IN
                                               i<k OR (i=k AND j<l)


  wf_lsth: LEMMA well_founded?[[nat,nat]](lsth) 

  p: VAR [[nat,nat]-> bool]

  gh: VAR [nat,nat]

  NAT_pair_induct: LEMMA (FORALL gh: LET (g,h) = gh IN 
                           (FORALL (l,m): lsth((l,m),(g,h))
                       IMPLIES p((l,m))) IMPLIES p((g,h)))
                           IMPLIES (FORALL (i,j): p((i,j)))

  IMPORTING graphs[T]


  G,H,GG,HH: VAR graph[T]

  P,Q: VAR [graph[T],graph[T] -> bool]

  size_up: LEMMA (FORALL (G,H): Q((G,H))) IFF 
                     (FORALL (G,H): (FORALL (m,n) :
                 (size(G),size(H)) = (m, n) IMPLIES Q((G,H))))

  graph_induct_pair    : THEOREM (FORALL (G,H): (FORALL (GG,HH): 
                                 (size(GG) < size(G) OR
                                 (size(GG)=size(G) AND size(HH) < size(H) ))
                                    IMPLIES Q((GG,HH)))
                                       IMPLIES Q((G,H)))
                                          IMPLIES (FORALL (G,H): Q((G,H)))

  graph_induct_pair_B  : THEOREM (FORALL (G,H): (FORALL (GG,HH): 
                                  lsth((size(GG),size(HH)),(size(G),size(H))) 
                                  IMPLIES Q((GG,HH)))
                                     IMPLIES Q((G,H)))
                                        IMPLIES (FORALL (G,H): Q((G,H)))

  graph_pair_induct_not: THEOREM (FORALL (G,H): P(G,H) IMPLIES
                                   (EXISTS (GG,HH): (size(GG) < size(G) 
                            OR (size(GG) = size(G) AND size(HH) < size(H)))
              AND P(GG,HH)))
                                     IMPLIES (FORALL (G,H): NOT P(G,H))



END graph_pair