fact: Definition relate' (p : pos_atom) (q : pos_atom) : atom_relation := match p, q with | Abnd px pi, Abnd qx qi => if index_eq px qx then compare pi qi else ARunknown | Abnd px pi, Aleq qx qu => if index_eq px qx then if Fle2 (upper pi) qu then ARimply else if Flt2 qu (lower pi) then ARcontradict else ARunknown else ARunknown | Abnd px pi, Ageq qx ql => if index_eq px qx then if Fle2 ql (lower pi) then ARimply else if Flt2 (upper pi) ql then ARcontradict else ARunknown else ARunknown | Aabs px pi, Aabs qx qi => if index_eq px qx then if Fpos0 (lower qi) then compare pi qi else ARunknown else ARunknown | Arel px py pi, Arel qx qy qi => if index_eq px qx then if index_eq py qy then if subset pi qi then ARimply else ARunknown else ARunknown else ARunknown | Afix px pc, Afix qx qc => if index_eq px qx then if Zle_bool qc pc then ARimply else ARunknown else ARunknown | Aflt px pc, Aflt qx qc => if index_eq px qx then if Zle_bool (Zpos pc) (Zpos qc) then ARimply else ARunknown else ARunknown | Anzr px, Anzr qx => if index_eq px qx then ARimply else ARunknown | Aeql px py, Aeql qx qy => if index_eq px qx then if index_eq py qy then ARimply else ARunknown else ARunknown | Aleq px pu, Abnd qx qi => if index_eq px qx then if Flt2 pu (lower qi) then ARcontradict else ARunknown else ARunknown | Aleq px pu, Aleq qx qu => if index_eq px qx then if Fle2 pu qu then ARimply else ARunknown else ARunknown | Aleq px pu, Ageq qx ql => if index_eq px qx then if Flt2 pu ql then ARcontradict else ARunknown else ARunknown | Ageq px pl, Abnd qx qi => if index_eq px qx then if Flt2 (upper qi) pl then ARcontradict else ARunknown else ARunknown | Ageq px pl, Aleq qx qu => if index_eq px qx then if Flt2 qu pl then ARcontradict else ARunknown else ARunknown | Ageq px pl, Ageq qx ql => if index_eq px qx then if Fle2 ql pl then ARimply else ARunknown else ARunknown | _, _ => ARunknown end.
imports: Reals List Bool Gappa_common