genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.thy 312 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
theory genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_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
begin

why3_open "genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"

why3_vc Grandparent_is_grandfather_or_grandmother
by (metis grandfather_def grandmother_def grandparent_def parent_def)

why3_end

end