Nuprl - Proof: assert-member-paren 1

(4steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: assert-member-paren 1

1. T: Type
2. E: TT
3. x,y:T. E(x,y) x = y
4. i: T
5. s: (T+T) List
6. i1: ||s||
7. InjCase(s[i1]; a. E(a,i), E(a,i))

(i@0:. i@0 < ||s|| & inl(i) = s[i@0]) (i@0:. i@0 < ||s|| & inr(i) = s[i@0])

By: MoveToConcl -1 THEN GenConcl (s[i1] = x) THEN Analyze -2 THEN Reduce 0

Generated subgoals:

1 7. x1: T
8. s[i1] = inl(x1)
9. E(x1,i)
(i@0:. i@0 < ||s|| & inl(i) = s[i@0]) (i@0:. i@0 < ||s|| & inr(i) = s[i@0]) 1 step

2 7. y: T
8. s[i1] = inr(y)
9. E(y,i)
(i@0:. i@0 < ||s|| & inl(i) = s[i@0]) (i@0:. i@0 < ||s|| & inr(i) = s[i@0]) 1 step

About:

(4steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc