Step * 1 1 of Lemma int_formula_prop_not_lemma

`1. x : Top@i`
`2. f : Top@i`
`⊢ ¬int_formula_ind(x;`
`                   intformless(left,right)`` int_term_value(f;left) < int_term_value(f;right);`
`                   intformle(left,right)`` int_term_value(f;left) ≤ int_term_value(f;right);`
`                   intformeq(left,right)`` int_term_value(f;left) = int_term_value(f;right) ∈ ℤ;`
`                   intformand(left,right)`` rec1,rec2.rec1 ∧ rec2;`
`                   intformor(left,right)`` rec3,rec4.rec3 ∨ rec4;`
`                   intformimplies(left,right)`` rec5,rec6.rec5 `` rec6;`
`                   intformnot(form)`` rec7.¬rec7)  ~ ¬int_formula_prop(f;x)`
BY
`{ Try (RW (AddrC [2] (UnfoldC `int_formula_prop`)) 0)⋅ }`

1
`1. x : Top@i`
`2. f : Top@i`
`⊢ ¬int_formula_ind(x;`
`                   intformless(left,right)`` int_term_value(f;left) < int_term_value(f;right);`
`                   intformle(left,right)`` int_term_value(f;left) ≤ int_term_value(f;right);`
`                   intformeq(left,right)`` int_term_value(f;left) = int_term_value(f;right) ∈ ℤ;`
`                   intformand(left,right)`` rec1,rec2.rec1 ∧ rec2;`
`                   intformor(left,right)`` rec3,rec4.rec3 ∨ rec4;`
`                   intformimplies(left,right)`` rec5,rec6.rec5 `` rec6;`
`                   intformnot(form)`` rec7.¬rec7)  ~ ¬int_formula_ind(x;`
`                                                                      a,b.int_term_value(f;a) < int_term_value(f;b);`
`                                                                      a,b.int_term_value(f;a) ≤ int_term_value(f;b);`
`                                                                      a,b.int_term_value(f;a) = int_term_value(f;b) ∈ ℤ;`
`                                                                      X,Y,PX,PY.PX ∧ PY;`
`                                                                      X,Y,PX,PY.PX ∨ PY;`
`                                                                      X,Y,PX,PY.PX `` PY;`
`                                                                      X,PX.¬PX)`

Latex:

Latex:

1.  x  :  Top@i
2.  f  :  Top@i
\mvdash{}  \mneg{}int\_formula\_ind(x;
intformless(left,right){}\mRightarrow{}  int\_term\_value(f;left)  <  int\_term\_value(f;right);
intformle(left,right){}\mRightarrow{}  int\_term\_value(f;left)  \mleq{}  int\_term\_value(f;right);
intformeq(left,right){}\mRightarrow{}  int\_term\_value(f;left)  =  int\_term\_value(f;right);
intformand(left,right){}\mRightarrow{}  rec1,rec2.rec1  \mwedge{}  rec2;
intformor(left,right){}\mRightarrow{}  rec3,rec4.rec3  \mvee{}  rec4;
intformimplies(left,right){}\mRightarrow{}  rec5,rec6.rec5  {}\mRightarrow{}  rec6;
intformnot(form){}\mRightarrow{}  rec7.\mneg{}rec7)    \msim{}  \mneg{}int\_formula\_prop(f;x)

By

Latex:
Try  (RW  (AddrC  [2]  (UnfoldC  `int\_formula\_prop`))  0)\mcdot{}

Home Index