Nuprl Lemma : eq_id_test
("x" = "x" ~ tt) ∧ ("x" = "y" ~ ff)
Proof
Definitions occuring in Statement :
eq_id: a = b,
mkid: "$x",
bfalse: ff,
btrue: tt,
and: P ∧ Q,
sqequal: s ~ t
Definitions unfolded in proof :
mkid: "$x",
eq_id: a = b,
id-deq: IdDeq,
atom2-deq: Atom2Deq,
eq_atom: eq_atom$n(x;y),
and: P ∧ Q,
cand: A c∧ B
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
independent_pairFormation,
hypothesis
Latex:
("x" = "x" \msim{} tt) \mwedge{} ("x" = "y" \msim{} ff)
Date html generated:
2016_05_14-PM-03_37_28
Last ObjectModification:
2015_12_26-PM-05_58_38
Theory : decidable!equality
Home
Index