ILE Home Intuitionistic Logic Explorer This is the GIF version.
Change to Unicode version

Symbol to ASCII Correspondence for Text-Only Browsers (in order of appearance in $c and $v statements in the database)

SymbolASCII
 ( (
 ) )
 ->  ->
 -.  -.
 wff  wff
 |-  |-
&  &
=>  =>
 ph ph
 ps ps
 ch ch
 th th
 ta ta
 et et
 ze ze
 si si
 rh rh
 mu mu
 la la
 ka ka
 /\  /\

<->  <->
 \/  \/
STAB  STAB
DECID  DECID
 A. A.
 setvar  setvar
 x x
 class  class
 =  =
 A A
 B B
T.  T.
 y y
F.  F.
 \/_  \/_
 z z
 w w
 v v
 u u
 t t
 F/ F/
 E. E.
 [ [
 /  /
 ] ]
 f f
 g g
 s s
 E! E!
 E* E*
 e.  e.
 { {
 |  |
 } }
 ./\  ./\
 .\/  .\/
 .<_  .<_
 .<  .<
 .+  .+
 .-  .-
 .X.  .X.
 ./  ./
 .^  .^
 .0.  .0.
 .1.  .1.
 .||  .||
 .~  .~
 ._|_  ._|_
 .+^  .+^
 .+b  .+b
 .(+)  .(+)
 .*  .*
 .x.  .x.
 .xb  .xb
 .,  .,
 .(x)  .(x)
 .o.  .o.
 .0b  .0b
 C C
 D D
 P P
 Q Q
 R R
 S S
 T T
 U U
 e e
 h h
 i i
 j j
 k k
 m m
 n n
 o o
 E E
 F F
 G G
 H H
 I I
 J J
 K K
 L L
 M M
 N N
 V V
 W W
 X X
 Y Y
 Z Z
 O O
 r r
 q q
 p p
 a a
 b b
 c c
 d d
 l l
 F/_ F/_
 =/=  =/=
 e/  e/
 _V _V
CondEq CondEq
 [. [.
 ]. ].
 [_ [_
 ]_ ]_
 \  \
 u.  u.
 i^i  i^i
 C_  C_
 (/) (/)
 ,  ,
 if if
 ~P ~P
 <. <.
 >. >.
 U. U.
 |^| |^|
 U_ U_
 |^|_ |^|_
Disj  Disj_
 |->  |->
 Tr  Tr
EXMID EXMID
 _E  _E
 _I  _I
 Po  Po
 Or  Or
FrFor  FrFor
 Fr  Fr
Se  Se
 We  We
 Ord  Ord
 On On
 Lim  Lim
 suc  suc
 om _om
 X.  X.
 `' `'
 dom  dom
 ran  ran
 |`  |`
 " "
 o.  o.
 Rel  Rel
 iota iota
 : :
 Fun  Fun
 Fn  Fn

--> -->
 -1-1-> -1-1->
 -onto-> -onto->

-1-1-onto-> -1-1-onto->
 `  `
 Isom  Isom
 iota_ iota_
 oF oF
 oR oR
 1st 1st
 2nd 2nd
tpos  tpos
 Smo  Smo
recs recs
 rec rec
frec frec
 1o 1o
 2o 2o
 3o 3o
 4o 4o
 +o  +o
 .o  .o
o  ^oi
 Er  Er
 /. /.
 ^m  ^m
 ^pm  ^pm
 X_ X_
 ~~  ~~
 ~<_  ~<_
 Fin Fin
 fi fi
 sup sup
inf inf
⊔  |_|
inl inl
inr inr
case case
⊔d  |_|d
 NN+oo
Omni Omni
Markov Markov
WOmni WOmni
 card card
CHOICE CHOICE
CCHOICE CCHOICE
 N. N.
 +N  +N
 .N  .N
 <N  <N
 +pQ  +pQ
 .pQ  .pQ
 <pQ  <pQ
 ~Q  ~Q
 Q. Q.
 1Q 1Q
 +Q  +Q
 .Q  .Q
 *Q *Q
 <Q  <Q
~Q0  ~Q0
Q0 Q0.
0Q0 0Q0
+Q0  +Q0
·Q0  .Q0
 P. P.
 1P 1P
 +P.  +P.
 .P.  .P.
 <P  <P
 ~R  ~R
 R. R.
 0R 0R
 1R 1R
 -1R -1R
 +R  +R
 .R  .R
 <R  <R
 <RR  <RR
 CC CC
 RR RR
 0 0
 1 1
 _i _i
 +  +
 x.  x.
 <_  <_
+oo +oo
-oo -oo
 RR* RR*
 <  <
 -  -
 -u -u
#  #RR
#  =//=
 NN NN
 2 2
 3 3
 4 4
 5 5
 6 6
 7 7
 8 8
 9 9
 NN0 NN0
NN0* NN0*
 ZZ ZZ
; ;
 ZZ>= ZZ>=
 QQ QQ
 RR+ RR+
 -e -e
 +e +e
 xe *e
 (,) (,)
 (,] (,]
 [,) [,)
 [,] [,]
 ... ...
..^ ..^
 |_ |_
⌈ |^
 mod  mod
 ==  ==
 seq seq
 ^ ^
 ! !
 _C  _C
♯ #
 shift  shift
 Re Re
 Im Im
 * *
 sqr sqrt
 abs abs
 pm +-

~~>  ~~>
 sum_ sum_
 prod_ prod_
 exp exp
 _e _e
 sin sin
 cos cos
 tan tan
 pi _pi
 tau _tau
 ||  ||
 gcd  gcd
lcm  lcm
 Prime Prime
numer numer
denom denom
 odZ odZ
 phi phi
 pCnt  pCnt
 ZZ[_i] Z[i]
Struct  Struct
 ndx ndx
sSet  sSet
Slot  Slot
 Base Base
s  |`s
 +g  +g
 .r .r
 *r *r
Scalar Scalar
 .s .s
 .i .i
TopSet TopSet
 le le
 oc oc
 dist dist
 UnifSet UnifSet
 Hom  Hom
comp comp
t  |`t
 TopOpen TopOpen
 topGen topGen
 Xt_ Xt_
 0g 0g
 gsumg  gsum
 X_s Xs_
 ^s  ^s
 +f +f
Mgm Mgm
Smgrp Smgrp
 Mnd Mnd
MndHom  MndHom
SubMnd SubMnd
 Grp Grp
 invg invg
 -g -g
PsMet PsMet
 *Met *Met
 Met Met
 ball ball
 fBas fBas
 filGen filGen
 MetOpen MetOpen
metUnif metUnif
 Top Top
TopOn TopOn
 TopSp TopSp
 TopBases TopBases
 int int
 cls cls
 Clsd Clsd
 nei nei
 Cn  Cn
 CnP  CnP

~~> t ~~>t
 tX  tX
 Homeo Homeo
 *MetSp *MetSp
 MetSp MetSp
toMetSp toMetSp
 -cn-> -cn->
lim CC  limCC
 _D  _D
 log log
 ^c  ^c
logb  logb
 /L /L
DECIDin  DECID_in
Δ0 Delta0
BOUNDED  Bdd
BOUNDED  Bdd_
Ind  Ind
 A.A!
  Copyright terms: Public domain W3C validator