Commit 00b36766 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update sessions

parent 792dde18
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+
......
<theory name="Child_is_son_or_daughter"><realized><require name="why3.BuiltIn"/></realized><typedecl name="person"><params/></typedecl><datatypes><datatype name="gender"><params/><constrs><constr name="Male"/><constr name="Female"/></constrs></datatype></datatypes><param name="gender1"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></param><param name="father"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><param name="mother"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><axiom name="Father_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></concls></axiom><axiom name="Mother_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></concls></axiom><definition><app><const name="HOL.eq"/><app><var name="parent"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="son"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="s"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="daughter"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="d"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="d"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="d"><type name="person" local="true"/></var></app></app></app></definition><lemma name="Child_is_son_or_daughter"><prems/><concls><app><const name="HOL.eq"/><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="son" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="c"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="daughter" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="c"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="Child_is_son_or_daughter"><realized><require name="why3.BuiltIn.BuiltIn"/></realized><typedecl name="person" altname="person"><params/></typedecl><datatypes><datatype name="gender" altname="gender"><params/><constrs><constr name="Male" altname="Male"/><constr name="Female" altname="Female"/></constrs></datatype></datatypes><param name="gender1" altname="gender"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></param><param name="father" altname="father"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><param name="mother" altname="mother"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><axiom name="Father_gender" altname="Father_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></concls></axiom><axiom name="Mother_gender" altname="Mother_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></concls></axiom><definition altname="parent"><app><const name="HOL.eq"/><app><var name="parent"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app></app></app></definition><definition altname="son"><app><const name="HOL.eq"/><app><var name="son"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="s"><type name="person" local="true"/></var></app></app></app></definition><definition altname="daughter"><app><const name="HOL.eq"/><app><var name="daughter"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="d"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="d"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="d"><type name="person" local="true"/></var></app></app></app></definition><lemma name="Child_is_son_or_daughter" altname="Child_is_son_or_daughter"><prems/><concls><app><const name="HOL.eq"/><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="son" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="c"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="daughter" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="c"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="Sibling_is_brother_or_sister"><realized><require name="why3.BuiltIn"/></realized><typedecl name="person"><params/></typedecl><datatypes><datatype name="gender"><params/><constrs><constr name="Male"/><constr name="Female"/></constrs></datatype></datatypes><param name="gender1"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></param><param name="father"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><param name="mother"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><axiom name="Father_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></concls></axiom><axiom name="Mother_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></concls></axiom><definition><app><const name="HOL.eq"/><app><var name="parent"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="son"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="s"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="daughter"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="d"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="d"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="d"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="sibling"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="brother"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="b"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="b"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="b"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="sister"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></app></app></definition><lemma name="Sibling_is_brother_or_sister"><prems/><concls><app><const name="HOL.eq"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="brother" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="sister" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="Sibling_is_brother_or_sister"><realized><require name="why3.BuiltIn.BuiltIn"/></realized><typedecl name="person" altname="person"><params/></typedecl><datatypes><datatype name="gender" altname="gender"><params/><constrs><constr name="Male" altname="Male"/><constr name="Female" altname="Female"/></constrs></datatype></datatypes><param name="gender1" altname="gender"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></param><param name="father" altname="father"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><param name="mother" altname="mother"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><axiom name="Father_gender" altname="Father_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></concls></axiom><axiom name="Mother_gender" altname="Mother_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></concls></axiom><definition altname="parent"><app><const name="HOL.eq"/><app><var name="parent"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app></app></app></definition><definition altname="son"><app><const name="HOL.eq"/><app><var name="son"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="s"><type name="person" local="true"/></var></app></app></app></definition><definition altname="daughter"><app><const name="HOL.eq"/><app><var name="daughter"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="d"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="d"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="d"><type name="person" local="true"/></var></app></app></app></definition><definition altname="sibling"><app><const name="HOL.eq"/><app><var name="sibling"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app></app></app></app></definition><definition altname="brother"><app><const name="HOL.eq"/><app><var name="brother"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="b"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="b"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="b"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></app></app></definition><definition altname="sister"><app><const name="HOL.eq"/><app><var name="sister"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></app></app></definition><lemma name="Sibling_is_brother_or_sister" altname="Sibling_is_brother_or_sister"><prems/><concls><app><const name="HOL.eq"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="brother" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="sister" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment