Nuprl - Proof: paren order1

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

T:Type, s:(T+T) List. paren(T;s) (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2))

By: Analyze 0 THEN BackThru Thm* paren_induction

Generated subgoals:

1 1. T: Type
i:T, s1,s2:(T+T) List. nil = (s1 @ [inl(i)] @ s2) (inr(i) s2) 1 step

2 1. T: Type
s1,s2:(T+T) List. (i:T, s1@0,s2:(T+T) List. s1 = (s1@0 @ [inl(i)] @ s2) (inr(i) s2)) (i:T, s1,s2@0:(T+T) List. s2 = (s1 @ [inl(i)] @ s2@0) (inr(i) s2@0)) paren(T;s1) paren(T;s2) (i:T, s1@0,s2@0:(T+T) List. (s1 @ s2) = (s1@0 @ [inl(i)] @ s2@0) (inr(i) s2@0)) 14 steps

3 1. T: Type
s:(T+T) List, t:T. (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)) paren(T;s) (i:T, s1,s2:(T+T) List. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(i)] @ s2) (inr(i) s2)) 31 steps

About:

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

1	1. `T:` `Type` `i:T, s1,s2:(T+T) List. nil = (s1 @ [inl(i)] @ s2) (inr(i) s2)`	1 step

2	1. `T:` `Type` `s1,s2:(T+T) List. (i:T, s1@0,s2:(T+T) List. s1 = (s1@0 @ [inl(i)] @ s2) (inr(i) s2)) (i:T, s1,s2@0:(T+T) List. s2 = (s1 @ [inl(i)] @ s2@0) (inr(i) s2@0)) paren(T;s1) paren(T;s2) (i:T, s1@0,s2@0:(T+T) List. (s1 @ s2) = (s1@0 @ [inl(i)] @ s2@0) (inr(i) s2@0))`	14 steps

3	1. `T:` `Type` `s:(T+T) List, t:T. (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)) paren(T;s) (i:T, s1,s2:(T+T) List. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(i)] @ s2) (inr(i) s2))`	31 steps