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
♯	#
shift	shift
ℜ	Re
ℑ	Im
∗	*
√	sqrt
abs	abs
±	+-
⇝	~~>
Σ	sum_
∏	prod_
exp	exp
e	_e
sin	sin
cos	cos
tan	tan
π	_pi
τ	_tau
∥	||
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
CMnd	CMnd
Abel	Abel
mulGrp	mulGrp
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
SubRing	SubRing
RingSpan	RingSpan
#r	#r
PsMet	PsMet
∞Met	*Met
Met	Met
ball	ball
fBas	fBas
filGen	filGen
MetOpen	MetOpen
metUnif	metUnif
ℂfld	CCfld
ℤring	ZZring
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
log	log
↑𝑐	^c
logb	logb
/L	/L
DECIDin	DECID_in
Δ0	Delta0
BOUNDED	Bdd
BOUNDED	Bdd_
Ind	Ind
∀!	A!