(* Verification Conditions for Alt-Ergo *)

type letter = A | B | C | D | F
logic map : int -> letter
axiom A1: forall n: int. ((n>90)  ->
     map(n)=A)
 and 
((n>70) and 
n<=90  ->
     map(n)=B)
 and 
((n>50) and 
n<=70  ->
     map(n)=C)
 and 
((n>30) and 
n<=50  ->
     map(n)=D)
 and 
(n<=30  ->
     map(n)=F)


logic marks: int
logic grade: letter

goal start:
(55<=marks<=65  ->
     map(marks)=C)