Step * 1 of Lemma int_formula_prop_not_lemma

`1. x : Top@i`
`2. f : Top@i`
`⊢ int_formula_prop(f;"¬"x) ~ ¬int_formula_prop(f;x)`
BY
`{ Try (RW (AddrC [1] (UnfoldC `int_formula_prop` ANDTHENC ReduceC)) 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_prop(f;x)`

Latex:

Latex:

1.  x  :  Top@i
2.  f  :  Top@i
\mvdash{}  int\_formula\_prop(f;"\mneg{}"x)  \msim{}  \mneg{}int\_formula\_prop(f;x)

By

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

Home Index