Go backward to The Union Theorem
Go up to Top
Go forward to Collaries

Proof of Union Theorem

Only second case is not straight-forward.

$p$ ensures $q$ in $F$ [] $G$
$<=>$ $p$ unless $q$ in $F$ [] $G$
   and <exists $s$ : $s$ in $F$ [] $q$ :: { $p$ and not $q$ } $s$ { $q$ }>
$<=>$ $p$ unless $q$ in $F$ [] $G$
   and [<exists $s$ : $s$ in $F$ :: { $p$ and not $q$ } $s$ { $q$ }>
      or <exists $s$ : $s$ in $G$ :: { $p$ and not $q$ } $s$ { $q$ }>]
$<=>$ [ $p$ unless $q$ in $F$ [] $G$
      and <exists $s$ : $s$ in $F$ :: { $p$ and not $q$ } $s$ { $q$ }>] or
   [ $p$ unless $q$ in $F$ [] $G$
      and <exists $s$ : $s$ in $G$ :: { $p$ and not $q$ } $s$ { $q$ }>]
$<=>$ [ $p$ unless $q$ in $F$ and $p$ unless $q$ in $G$
      and <exists $s$ : $s$ in $F$ :: { $p$ and not $q$ } $s$ { $q$ }>] or
   [ $p$ unless $q$ in $F$ and $p$ unless $q$ in $G$
      and <exists $s$ : $s$ in $G$ :: { $p$ and not $q$ } $s$ { $q$ }>]
$<=>$ [ $p$ ensures $q$ in $F$ and $p$ unless $q$ in $G$ ] or
   [ $p$ ensures $q$ in $G$ and $p$ unless $q$ in $F$ ]

Wolfgang.Schreiner@risc.uni-linz.ac.at

Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine