genealogy_Genealogy_Child_is_son_or_daughter_1.thy 405 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
theory genealogy_Genealogy_Child_is_son_or_daughter_1
Stefan Berghofer's avatar
Stefan Berghofer committed
2
imports Why3.Why3
MARCHE Claude's avatar
MARCHE Claude committed
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
begin

why3_open "genealogy_Genealogy_Child_is_son_or_daughter_1.xml"

why3_vc Child_is_son_or_daughter
proof -
  have "parent p c \<longrightarrow> son c p \<or> gender1 c = Female"
    using gender.exhaust son_def by auto
  thus "parent p c = (son c p \<or> daughter c p)"
    using daughter_def son_def by auto
qed

why3_end

end