Child_is_son_or_daughter: THEORY
 BEGIN
  % do not edit above this line
  % surround new declarations you insert below with blank lines
  
  % Why3 person
  person: TYPE+
  
  % Why3 gender
  gender: DATATYPE
   BEGIN
    male: male?
    female: female?
   END gender
  
  % Why3 gender1
  gender1(x:person): gender
  
  % Why3 father
  father(x:person): person
  
  % Why3 mother
  mother(x:person): person
  
  % Why3 father_gender
  father_gender: AXIOM FORALL (p:person): (gender1(father(p)) = male)
  
  % Why3 mother_gender
  mother_gender: AXIOM FORALL (p:person): (gender1(mother(p)) = female)
  
  % Why3 parent
  parent(p:person, c:person): bool = (p = father(c)) OR (p = mother(c))
  
  % Why3 son
  son(s:person, p:person): bool = (gender1(s) = male) AND parent(p, s)
  
  % Why3 daughter
  daughter(d:person, p:person): bool = (gender1(d) = female) AND parent(p, d)
  
  % Why3 child
  child(c:person, p:person): bool = parent(p, c)
  
  % Why3 child_is_son_or_daughter
  child_is_son_or_daughter: THEOREM FORALL (c:person, p:person): child(c,
    p) <=> (son(c, p) OR daughter(c, p))
  
  
 END Child_is_son_or_daughter
 