Nuprl - Proof: flip lemma 2

(17steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: flip lemma 2

1. k :

2. x :

k
3. y :

k
4. z :

k
5.

y = z
6.

x = y
7. x1 :

k
8.

x1 = x

if x1=

x else x1 fi

if if if x1=

x else x1 fi=

if i; if x1=

x else x1 fi=

if i; x1=

if else x1 fi=

if z

i; if if x1=

x else x1 fi=

i; i; if x1=

x else x1 fi=

i; i; x1=

i; else x1 fi=

i; x

i; if x1=

x else x1 fi=

i; if x1=

x else x1 fi=

i; x1=

else x1 fi

By:	SplitOnConclITE

Generated subgoals:

1 9. x1 = y
  x
  =
  if if if x1=z x else x1 fi=y z
  if i; if x1=z x else x1 fi=z y
  if i; x1=z x
  if else x1 fi=x
  if z
  i; if if x1=z x else x1 fi=y z
  i; i; if x1=z x else x1 fi=z y
  i; i; x1=z x
  i; else x1 fi=z
  i; x
  i; if x1=z x else x1 fi=y z
  i; if x1=z x else x1 fi=z y
  i; x1=z x
  else x1 fi
3 steps

2 9. x1 = y
  x1
  =
  if if if x1=z x else x1 fi=y z
  if i; if x1=z x else x1 fi=z y
  if i; x1=z x
  if else x1 fi=x
  if z
  i; if if x1=z x else x1 fi=y z
  i; i; if x1=z x else x1 fi=z y
  i; i; x1=z x
  i; else x1 fi=z
  i; x
  i; if x1=z x else x1 fi=y z
  i; if x1=z x else x1 fi=z y
  i; x1=z x
  else x1 fi
7 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(17steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

1	9. x1 = y x = if if if x1=z x else x1 fi=y z if i; if x1=z x else x1 fi=z y if i; x1=z x if else x1 fi=x if z i; if if x1=z x else x1 fi=y z i; i; if x1=z x else x1 fi=z y i; i; x1=z x i; else x1 fi=z i; x i; if x1=z x else x1 fi=y z i; if x1=z x else x1 fi=z y i; x1=z x else x1 fi	3 steps
2	9. x1 = y x1 = if if if x1=z x else x1 fi=y z if i; if x1=z x else x1 fi=z y if i; x1=z x if else x1 fi=x if z i; if if x1=z x else x1 fi=y z i; i; if x1=z x else x1 fi=z y i; i; x1=z x i; else x1 fi=z i; x i; if x1=z x else x1 fi=y z i; if x1=z x else x1 fi=z y i; x1=z x else x1 fi	7 steps