Step * 2 of Lemma proper-iseg-append


1. Type
2. T
3. List
4. ∀L2,L3,L4:T List.  L3 < L2 L4 ⇐⇒ L3 < L4 ∧ (v L2 ∈ (T List)) supposing ||v|| ||L2|| ∈ ℤ
5. u1 T
6. v1 List
7. ∀L3,L4:T List.  [u v] L3 < v1 L4 ⇐⇒ L3 < L4 ∧ ([u v] v1 ∈ (T List)) supposing ||[u v]|| ||v1|| ∈ ℤ
8. L3 List
9. L4 List
10. (||v|| 1) (||v1|| 1) ∈ ℤ
11. [u (v L3)] < [u1 (v1 L4)]
⊢ [u v] [u1 v1] ∈ (T List)
BY
((RWO "cons-proper-iseg" (-1) THENA Auto) THEN EqCD THEN Auto THEN InstHyp [⌜v1⌝;⌜L3⌝;⌜L4⌝4⋅ THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}L2,L3,L4:T  List.    v  @  L3  <  L2  @  L4  \mLeftarrow{}{}\mRightarrow{}  L3  <  L4  \mwedge{}  (v  =  L2)  supposing  ||v||  =  ||L2||
5.  u1  :  T
6.  v1  :  T  List
7.  \mforall{}L3,L4:T  List.
          [u  /  v]  @  L3  <  v1  @  L4  \mLeftarrow{}{}\mRightarrow{}  L3  <  L4  \mwedge{}  ([u  /  v]  =  v1)  supposing  ||[u  /  v]||  =  ||v1||
8.  L3  :  T  List
9.  L4  :  T  List
10.  (||v||  +  1)  =  (||v1||  +  1)
11.  [u  /  (v  @  L3)]  <  [u1  /  (v1  @  L4)]
\mvdash{}  [u  /  v]  =  [u1  /  v1]


By


Latex:
((RWO  "cons-proper-iseg"  (-1)  THENA  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}L3\mkleeneclose{};\mkleeneopen{}L4\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)




Home Index