Step | Hyp | Ref
| Expression |
1 | | elex 2748 |
. 2
![( (](lp.gif) Omni ![_V _V](rmcv.gif) ![) )](rp.gif) |
2 | | simpl 109 |
. . 3
![( (](lp.gif) ![( (](lp.gif) WOmni
Markov
WOmni![) )](rp.gif) |
3 | 2 | elexd 2750 |
. 2
![( (](lp.gif) ![( (](lp.gif) WOmni
Markov
![_V _V](rmcv.gif) ![) )](rp.gif) |
4 | | 1n0 6427 |
. . . . . . . . . . . . . . 15
![(/) (/)](varnothing.gif) |
5 | 4 | nesymi 2393 |
. . . . . . . . . . . . . 14
![1o 1o](_1o.gif) |
6 | | eqeq1 2184 |
. . . . . . . . . . . . . 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 675 |
. . . . . . . . . . . . 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 2574 |
. . . . . . . . . . . 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 2466 |
. . . . . . . . . . . 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 760 |
. . . . . . . . . 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 729 |
. . . . . . . . 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 835 |
. . . . . . . . 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 134 |
. . . . . . . 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 277 |
. . . . . . 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 110 |
. . . . . . . . 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 729 |
. . . . . . . 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 724 |
. . . . . . 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 306 |
. . . . . 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 529 |
. . . . . . . . 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 122 |
. . . . . . . 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 531 |
. . . . . . . . 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 788 |
. . . . . . . 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 729 |
. . . . . 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 596 |
. . . . 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 443 |
. . . 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 1824 |
. . 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 7128 |
. . 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 7157 |
. . . . . 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 7145 |
. . . . . 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 473 |
. . . . 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 1481 |
. . . . 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 198 |
. . . 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 603 |
. . . . 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 1470 |
. . . 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 198 |
. . 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 220 |
. 2
![( (](lp.gif) ![( (](lp.gif)
Omni ![( (](lp.gif) WOmni
Markov![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 1, 3, 38 | pm5.21nii 704 |
1
![( (](lp.gif) Omni ![( (](lp.gif) WOmni Markov![) )](rp.gif) ![) )](rp.gif) |