ratplus[x]

Johan G. F. Belinfante
2012 November 21

SetDirectory["l:"];  << goedel.12nov17a

summary

The function  ratplus[x]  is defined and some of its properties are derived.

derivation

Definition.

composite[RATADD, LEFT[x_]] := ratplus[x]

Theorem.  Simplification rule.

Assoc[RATADD, SWAP, LEFT[x]]

composite[RATADD, RIGHT[x_]] := ratplus[x]

Theorem.  The class  ratplus[x]  is a function.

SubstTest[FUNCTION, composite[binop[t], LEFT[x]], t -> RATADD] // 
      Reverse

FUNCTION[ratplus[x_]] := True

Theorem.  The domain of ratplus[x].

IminComp[RATADD, LEFT[x], V]

domain[ratplus[x_]] := 
      intersection[RATS, image[V, intersection[RATS, set[x]]]]

Corollary.

Assoc[ratplus[x], id[domain[ratplus[x]]], id[RATS]] // 
      Reverse

composite[ratplus[x_], id[RATS]] := ratplus[x]

Theorem.

SubstTest[empty, composite[t, LEFT[x]], t -> RATADD] // 
      Reverse

equal[0, ratplus[x_]] := not[member[x, RATS]]

Theorem.  Function application rule.

SubstTest[APPLY, composite[binop[t], LEFT[x]], y, t -> RATADD] // 
      Reverse

APPLY[ratplus[x_], y_] := ratadd[x, y]

Theorem.  Vertical section rule.

SubstTest[image, funpart[t], set[y], t -> ratplus[x]] // 
      Reverse

image[ratplus[x_], set[y_]] := set[ratadd[x, y]]

Theorem.

Assoc[composite[RATADD, cross[Id, RATADD]], ASSOC, RIGHT[x]] // 
      Reverse

composite[ratplus[x_], RATADD] := 
      composite[RATADD, cross[Id, ratplus[x]]]

Theorem.  Rule for composites.

Assoc[ratplus[x], RATADD, RIGHT[y]]

composite[ratplus[x_], ratplus[y_]] := ratplus[ratadd[x, y]]

The following rule is a replacement for an existing rewrite rule that will be removed.

Theorem.  Replacement rule.

SubstTest[composite, RATADD, LEFT[t], t -> e[RATADD]]

ratplus[cart[Z, set[id[omega]]]] := id[RATS]

Lemma.  Simplication rule.

composite[inverse[LEFT[x]], inverse[RATADD]] // 
      DoubleInverse

composite[inverse[LEFT[x_]], inverse[RATADD]] := 
      inverse[ratplus[x]]

Lemma.  Simplication rule.

composite[inverse[RIGHT[x]], inverse[RATADD]] // 
      DoubleInverse

composite[inverse[RIGHT[x_]], inverse[RATADD]] := 
      inverse[ratplus[x]]

Theorem.

Map[FUNCTION, 
      SubstTest[composite, flip[rotate[t]], LEFT[x], 
        t -> RATADD]]

FUNCTION[inverse[ratplus[x_]]] := True