Nuprl - Proof: assert-member-left-paren 1

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

At: assert-member-left-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), false)

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

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

Generated subgoal:

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

About:

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