this is for holding javascript data
Mazdak Farrokhzad edited Ex 1.tex
over 9 years ago
Commit id: b02928af9435c9e35cfb03e568bf8c8833cb130f
deletions | additions
diff --git a/Ex 1.tex b/Ex 1.tex
index 63271de..93d34cd 100644
--- a/Ex 1.tex
+++ b/Ex 1.tex
...
\newcommand{\if}[2]{if(#1) \ \{ #2 \}}
\newcommand{\else}[1]{else \ \{ #1 \}}
\newcommand{\ie}[3]{\if{#1}{#2} \ \else{#3}}
\newcommand{\a}[0]{\land}
Given:
\begin{equation}
\begin{split}
Q &= \empty\\
R &= 0 \leq y
\land \a (0 \leq x \to y = x)
\land \a (x < 0 \to y = -x)
\end{split}
\end{equation}
\begin{equation}
\begin{split}
& \wp{\ie{x < 0}{y := -x}{ y := x }}{R} \\
\iff & (x < 0 \to \wp{y:= -x}{R})
\land \a (0 \leq x \to \wp{y:= x}{R})\\
\iff & (x < 0 \to (0 \leq -x
\land \a (0 \leq x \to -x = x)
\land \a (x < 0 \to -x = -x )))\\
\land & (x \leq 0 \to (0 \leq x
\land \a (0 \leq x \to x = x)
\land \a (x < 0 \to x =
-x))) -x)))\\
\iff & (x < 0 \to -x = -x) \a (0 \leq x \to x = x)\\
\iff & T
\end{split}
\end{equation}