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

Re: instantiation




your thoerem is not true.

a3 < a4

AND

a4 < a3

could be true or false and still be consistent with the set of axioms
that you have defined.

You might wish to define some more.

You have assumed term is transitive, you might wish to add
anti_symmetric, and/or reflexivity.

These concepts are all defined in the prelude.

John

> 
> 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
> 
>