ramsey_new[T: TYPE]: THEORY
BEGIN
  IMPORTING graphs[T], subgraphs[T]
  i, j: VAR T

  n, p, q, ii: VAR nat   

%  g: VAR graph[T]
  g: VAR graph[T]
  V: VAR finite_set[T]

  contains_clique(g, n): bool =
      (EXISTS (C: finite_set[T]):
        subset?(C,vert(g)) AND card(C) >= n AND
          (FORALL i,j: i/=j AND C(i) AND C(j) IMPLIES edge?(g)(i,j)))

  contains_indep(g, n): bool =
      (EXISTS (D: finite_set[T]):
        subset?(D, vert(g)) AND card(D) >= n AND
         (FORALL i, j: i/=j AND D(i) AND D(j) IMPLIES NOT edge?(g)(i, j)))

  subgraph_clique: LEMMA (FORALL (V: set[T]): 
                             contains_clique(subgraph(g, V), p)
                             IMPLIES contains_clique(g, p))

  subgraph_indep : LEMMA (FORALL (V: set[T]): 
                             contains_indep(subgraph(g, V), p)
                             IMPLIES contains_indep(g, p))

  G: VAR Graph[T]   % finite and nonempty

  r1(G): finite_set[T] = (LET v0 = choose(vert(G)) IN
           { n: T | vert(G)(n) AND n /= v0 AND edge?(G)(v0,n)})

  r2(G): finite_set[T] = (LET v0 = choose(vert(G)) IN
           { n: T | vert(G)(n) AND n /= v0 AND NOT edge?(G)(v0,n)})


  SG1(G): graph[T] = subgraph(G, r1(G))

  SG2(G): graph[T] = subgraph(G, r2(G))

  v0: VAR nat
  card_r1_r2: LEMMA card(r1(G)) + card(r2(G)) >= size(G) - 1

%  ramsey(p, q): RECURSIVE posnat =
%         (IF p=0
%          THEN 1
%          ELSIF q=0
%             THEN 1
%             ELSE (ramsey(p-1,q)+ramsey(p, q-1))
%             ENDIF)
%  MEASURE p+q

  ramsey(p, q): posnat 

  l1,l2: VAR nat

  ramsey_lem: LEMMA (FORALL l1,l2: l1+l2=ii IMPLIES
      (EXISTS (n: posnat):
          (FORALL (G: Graph[T]): size(G) >= n
              IMPLIES (contains_clique(G, l1) OR
                       contains_indep(G, l2)))))


  ramseys_theorem: THEOREM (EXISTS (n: posnat):
                               (FORALL (G: Graph[T]): size(G) >= n
                                   IMPLIES (contains_clique(G, l1) OR
                                            contains_indep(G, l2))))



END ramsey_new