mmascii - Intuitionistic Logic Explorer

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

Symbol	ASCII
(	(
)	)
→	->
¬	-.
wff	wff
⊢	|-
&	&
⇒	=>
𝜑	ph
𝜓	ps
𝜒	ch
𝜃	th
𝜏	ta
𝜂	et
𝜁	ze
𝜎	si
𝜌	rh
𝜇	mu
𝜆	la
𝜅	ka
∧	/\
↔	<->
∨	\/
STAB	STAB
DECID	DECID
∀	A.
setvar	setvar
𝑥	x
class	class
=	=
𝐴	A
𝐵	B
⊤	T.
𝑦	y
⊥	F.
⊻	\/_
𝑧	z
𝑤	w
𝑣	v
𝑢	u
𝑡	t
Ⅎ	F/
∃	E.
[	[
/	/
]	]
𝑓	f
𝑔	g
𝑠	s
∃!	E!
∃*	E*
∈	e.
{	{
∣	|
}	}
∧	./\
∨	.\/
≤	.<_
<	.<
+	.+
−	.-
×	.X.
/	./
↑	.^
0	.0.
1	.1.
∥	.||
#	.#
∼	.~
⊥	._|_
⨣	.+^
✚	.+b
⊕	.(+)
∗	.*
·	.x.
∙	.xb
,	.,
⊗	.(x)
⚬	.o.
𝟎	.0b
𝐶	C
𝐷	D
𝑃	P
𝑄	Q
𝑅	R
𝑆	S
𝑇	T
𝑈	U
𝑒	e
ℎ	h
𝑖	i
𝑗	j
𝑘	k
𝑚	m
𝑛	n
𝑜	o
𝐸	E
𝐹	F
𝐺	G
𝐻	H
𝐼	I
𝐽	J
𝐾	K
𝐿	L
𝑀	M
𝑁	N
𝑉	V
𝑊	W
𝑋	X
𝑌	Y
𝑍	Z
𝑂	O
𝑟	r
𝑞	q
𝑝	p
𝑎	a
𝑏	b
𝑐	c
𝑑	d
𝑙	l
Ⅎ	F/_
≠	=/=
∉	e/
V	_V
CondEq	CondEq
[	[.
]	].
⦋	[_
⦌	]_
∖	\
∪	u.
∩	i^i
⊆	C_
∅	(/)
,	,
if	if
𝒫	~P
⟨	<.
⟩	>.
∪	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
×	X.
◡	`'
dom	dom
ran	ran
↾	|`
“	"
∘	o.
Rel	Rel
℩	iota
:	:
Fun	Fun
Fn	Fn
⟶	-->
–1-1→	-1-1->
–onto→	-onto->
–1-1-onto→	-1-1-onto->
‘	`
Isom	Isom
℩	iota_
∘𝑓	oF
∘𝑟	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
↑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
ℂ	CC
ℝ	RR
0	0
1	1
i	_i
+	+
·	x.
≤	<_
+∞	+oo
-∞	-oo
ℝ*	RR*
<	<
−	-
-	-u
#ℝ	#RR
#	=//=
ℕ	NN
2	2
3	3
4	4
5	5
6	6
7	7
8	8
9	9
ℕ0	NN0
ℕ0*	NN0*
ℤ	ZZ
;	;
ℤ≥	ZZ>=
ℚ	QQ
ℝ+	RR+
-𝑒	-e
+𝑒	+e
·e	*e
(,)	(,)
(,]	(,]
[,)	[,)
[,]	[,]
...	...
..^	..^
⌊	|_
⌈	|^
mod	mod
≡	==
seq	seq
↑	^
!	!
C	_C
♯	#
Word	Word
shift	shift
ℜ	Re
ℑ	Im
∗	*
√	sqrt
abs	abs
±	+-
⇝	~~>
Σ	sum_
∏	prod_
exp	exp
e	_e
sin	sin
cos	cos
tan	tan
π	_pi
τ	_tau
∥	||
bits	bits
gcd	gcd
lcm	lcm
ℙ	Prime
numer	numer
denom	denom
odℤ	odZ
ϕ	phi
pCnt	pCnt
ℤ[i]	Z[i]
Struct	Struct
ndx	ndx
sSet	sSet
Slot	Slot
Base	Base
↾s	|`s
+g	+g
.r	.r
*𝑟	*r
Scalar	Scalar
·𝑠	.s
·𝑖	.i
TopSet	TopSet
le	le
oc	oc
dist	dist
UnifSet	UnifSet
Hom	Hom
comp	comp
↾t	|`t
TopOpen	TopOpen
topGen	topGen
∏t	Xt_
0g	0g
Σg	gsum
Xs	Xs_
↑s	^s
“s	"s
/s	/s
×s	Xs.
+𝑓	+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
ℤRHom	ZRHom
ℤMod	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
Homeo	Homeo
∞MetSp	*MetSp
MetSp	MetSp
toMetSp	toMetSp
–cn→	-cn->
limℂ	limCC
D	_D
Poly	Poly
Xp	Xp
log	log
↑𝑐	^c
logb	logb
σ	sigma
/L	/L
DECIDin	DECID_in
Δ0	Delta0
BOUNDED	Bdd
BOUNDED	Bdd_
Ind	Ind
∀!	A!