Nuprl Lemma : atom-test1
'xxx'1 =a1 'yyy'1 = ff
Proof
Definitions occuring in Statement :
eq_atom: eq_atom$n(x;y),
token: '$x'1,
bfalse: ff,
bool: 𝔹,
equal: s = t ∈ T
Definitions unfolded in proof :
eq_atom: eq_atom$n(x;y),
member: t ∈ T
Lemmas referenced :
bfalse_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule,
cut,
lemma_by_obid,
hypothesis
Latex:
'xxx'1 =a1 'yyy'1 = ff
Date html generated:
2016_05_13-PM-03_21_20
Last ObjectModification:
2015_12_26-AM-09_11_57
Theory : atom_1
Home
Index