Step * 2 1 of Lemma ni-max-nat


1. : ℕ
2. : ℕ
3. : ℕ@i
4. ↑(i 1 <n ∨b1 <m)@i
⊢ ↑(i <n ∨bi <m)
BY
((All (RW assert_pushdownC) THENA Auto) THEN ParallelLast THEN Auto) }


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  i  :  \mBbbN{}@i
4.  \muparrow{}(i  +  1  <z  n  \mvee{}\msubb{}i  +  1  <z  m)@i
\mvdash{}  \muparrow{}(i  <z  n  \mvee{}\msubb{}i  <z  m)


By


Latex:
((All  (RW  assert\_pushdownC)  THENA  Auto)  THEN  ParallelLast  THEN  Auto)




Home Index