genealogy_Genealogy_Child_is_son_or_daughter_1.pvs 1.11 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3
Child_is_son_or_daughter: THEORY
 BEGIN
  % do not edit above this line
MARCHE Claude's avatar
MARCHE Claude committed
4
  % surround new declarations you insert below with blank lines
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
  
  % 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