Nuprl - Proof: flip lemma

(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

, x,y,z:

y = z

x = y

(x, y) = compose_list([(x, z); (y, z); (x, z)])

By:	Auto THEN Ext THEN Unfolds [`compose_list`] 0 THEN Reduce 0 THEN Unfold `flip` 0 THEN Reduce 0 THEN SplitOnConclITE

Generated subgoals:

1 1. k :
2. x : k
3. y : k
4. z : k
5. y = z
6. x = y
7. x1 : k
8. x1 = x
  y
  =
  if if z=y z ; z=z y else z fi=x z
  i; if z=y z ; z=z y else z fi=z x
  i; z=y z
  i; z=z y
  else z fi
5 steps

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=y x else x1 fi
  =
  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
11 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	1. k : 2. x : k 3. y : k 4. z : k 5. y = z 6. x = y 7. x1 : k 8. x1 = x y = if if z=y z ; z=z y else z fi=x z i; if z=y z ; z=z y else z fi=z x i; z=y z i; z=z y else z fi	5 steps
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=y x else x1 fi = 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	11 steps