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
Ap  Ap
TAp  TAp
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
♯ #
Word  Word
 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
 "s  "s
 /.s  /s
 X.s  Xs.
 +f +f
Mgm Mgm
Smgrp Smgrp
 Mnd Mnd
MndHom  MndHom
SubMnd SubMnd
 Grp Grp
 invg invg
 -g -g
.g .g
~QG  ~QG
SubGrp SubGrp
NrmSGrp NrmSGrp
 GrpHom  GrpHom
CMnd CMnd
 Abel Abel
mulGrp mulGrp
Rng Rng
 1r 1r
SRing SRing
 Ring Ring
 CRing CRing
oppr oppR
 ||r ||r
Unit Unit
Irred Irred
 invr invr
/r /r
RingHom  RingHom
RingIso  RingIso
NzRing NzRing
LRing LRing
SubRng SubRng
SubRing SubRing
RingSpan RingSpan
RLReg RLReg
Domn Domn
IDomn IDomn
#r #r
 LMod LMod
 .sf .sf
 LSubSp LSubSp
 LSpan LSpan
subringAlg  subringAlg
ringLMod ringLMod
LIdeal LIdeal
RSpan RSpan
2Ideal 2Ideal
PsMet PsMet
 *Met *Met
 Met Met
 ball ball
 fBas fBas
 filGen filGen
 MetOpen MetOpen
metUnif metUnif
fld CCfld
ring ZZring
 ZRHom ZRHom
 ZMod ZMod
ℤ/nℤ Z/nZ
mPwSer  mPwSer
 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
Poly Poly
 Xp Xp
 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