[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

instantiation



Hi.

I would like to prove THEOREM test in theory s :
Could you help me?
 
s: THEORY
  BEGIN
           
  term: TYPE = { a1,a2,a3,a4,a5} 
  < : PRED[[term, term]]
  trans : AXIOM FORALL (x,y,z:term):
              x < y AND y < z IMPLIES x < z
 
  ax0 : AXIOM a1 < a2  
  ax1 : AXIOM a2 < a4
  ax2 : AXIOM a3 < a5
  
  test : THEOREM FORALL (a,b:term):  NOT ((a<b) AND (b<a))
          
END s


-----
thkim@salmosa.kaist.ac.kr