Step | Hyp | Ref
| Expression |
1 | | elex 2720 |
. 2
![( (](lp.gif) Omni ![_V _V](rmcv.gif) ![) )](rp.gif) |
2 | | simpl 108 |
. . 3
![( (](lp.gif) ![( (](lp.gif) WOmni
Markov
WOmni![) )](rp.gif) |
3 | 2 | elexd 2722 |
. 2
![( (](lp.gif) ![( (](lp.gif) WOmni
Markov
![_V _V](rmcv.gif) ![) )](rp.gif) |
4 | | 1n0 6369 |
. . . . . . . . . . . . . . 15
![(/) (/)](varnothing.gif) |
5 | 4 | nesymi 2370 |
. . . . . . . . . . . . . 14
![1o 1o](_1o.gif) |
6 | | eqeq1 2161 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | 5, 6 | mtbiri 665 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
8 | 7 | reximi 2551 |
. . . . . . . . . . . 12
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![E. E.](exists.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
9 | | rexnalim 2443 |
. . . . . . . . . . . 12
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
10 | 8, 9 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
11 | 10 | orim1i 750 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 11 | orcomd 719 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | df-dc 821 |
. . . . . . . . 9
DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | 12, 13 | sylibr 133 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif)
DECID ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
15 | 14 | adantl 275 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif)
DECID ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
16 | | simpr 109 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 16 | orcomd 719 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | 17 | ord 714 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 15, 18 | jca 304 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif)
DECID
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | | simprl 521 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
21 | 20, 13 | sylib 121 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | | simprr 522 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 22 | orim2d 778 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | 21, 23 | mpd 13 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 24 | orcomd 719 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 19, 25 | impbida 586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 26 | pm5.74da 440 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 27 | albidv 1801 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A.
A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | | isomni 7058 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
Omni ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | | iswomni 7087 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
WOmni ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | | ismkv 7075 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
Markov ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 30, 31 | anbi12d 465 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) WOmni Markov ![( (](lp.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | | 19.26 1458 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 32, 33 | bitr4di 197 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) WOmni Markov ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | | jcab 593 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
DECID ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 35 | albii 1447 |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![1o 1o](_1o.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 34, 36 | bitr4di 197 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) WOmni Markov ![A. A.](forall.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) DECID ![A. A.](forall.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 28, 29, 37 | 3bitr4d 219 |
. 2
![( (](lp.gif) ![( (](lp.gif)
Omni ![( (](lp.gif) WOmni
Markov![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 1, 3, 38 | pm5.21nii 694 |
1
![( (](lp.gif) Omni ![( (](lp.gif) WOmni Markov![) )](rp.gif) ![) )](rp.gif) |