Step
*
1
1
of Lemma
le_witness
1. i : ℤ
2. j : ℤ
3. x1 : ¬less_than'(j;i)
4. x3 : i ∈ ℤ
5. x4 : j ∈ ℤ
⊢ <x1, x3, x4> = <λx.x, Ax, Ax> ∈ (i ≤ j)
BY
{ ((D -1 THEN D -2 THEN RepUR ``le`` 0) THEN EqCD) }
1
.....subterm..... T:t
1:n
1. i : ℤ
2. j : ℤ
3. x1 : ¬less_than'(j;i)
4. x3 : i = i ∈ ℤ
5. x4 : j = j ∈ ℤ
⊢ x1 = (λx.x) ∈ (¬less_than'(j;i))
2
.....subterm..... T:t
2:n
1. i : ℤ
2. j : ℤ
3. x1 : ¬less_than'(j;i)
4. x3 : i = i ∈ ℤ
5. x4 : j = j ∈ ℤ
⊢ <Ax, Ax> = <Ax, Ax> ∈ ((i ∈ ℤ) ∧ (j ∈ ℤ))
Latex:
Latex:
1. i : \mBbbZ{}
2. j : \mBbbZ{}
3. x1 : \mneg{}less\_than'(j;i)
4. x3 : i \mmember{} \mBbbZ{}
5. x4 : j \mmember{} \mBbbZ{}
\mvdash{} <x1, x3, x4> = <\mlambda{}x.x, Ax, Ax>
By
Latex:
((D -1 THEN D -2 THEN RepUR ``le`` 0) THEN EqCD)
Home
Index