(and
 (=> (and {<= X Y} {<= Y Z} {<= Z R} {<= R X} {<= S X}) (= (F Y) (F R)))
 (=> (and {<= X Y} {<= Y Z} {<= Z R} {<= R S} {<= S X}) (= X Z))
 (=> (= (F X) X) (= {+ (F (F X)) Y} {+ X Y}))
 (=> (and {<= X P} {<= P X}) (= (F X) (F P)))
 (=> (and {<= X Y} {<= X {+ 1 {* -1 Y}}}) {<= {* 2 X} 1})
 (not {< X X}))