   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   