Example Igor proofs

gistfile1.txt

prove rtrclreclem.subset
autoall
expand df-rtrclrec
conclude ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n )
  use fvmpti2
  distr:ante
  use iunex
  use relexpex
  and rewrite
use ax-mp
let $ph = E. n e. NN0 R C_ ( R ^r n )
use ax-mp
let $ph = ( 1 e. NN0 /\ R C_ ( R ^r 1 ) )
  use pm3.2i
  expand relexp1
  use ssid
  use relexp1
use rcla4e
  and rewrite
use ssiun
quit

prove dfrtrclrec2
expand df-rtrclrec
antedisp
autoall
conclude ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n )
  use fvmpti2
    and rewrite
  use iunex
  use relexpex
  and rewrite
conclude ( A U_ n e. NN0 ( R ^r n ) B <-> <. A , B >. e. U_ n e. NN0 ( R ^r n ) )
  use df-br
  and rewrite
conclude ( E. n e. NN0 A ( R ^r n ) B <-> E. n e. NN0 <. A , B >. e. ( R ^r n ) )
  use rexbii
  use df-br
  and rewrite
use eliun
quit

prove rtrclreclem.trans
autoall
antedisp
use mpbir
let $ps = A. d ( d e. ( ( t*rec ` R ) o. ( t*rec ` R ) ) -> d e. ( t*rec ` R ) )
  / C_
  use dfss2
use ax-gen
conclude ( ( t*rec ` R ) o. ( t*rec ` R ) ) = { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) }
  use df-co
  and rewrite
use sylbi
let $ps = E. e E. g ( d = <. e , g >. /\ E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) )
  use elopab
use exlimiv
use exlimiv
and rewrite
use exlimiv
conclude E. n e. NN0 e ( R ^r n ) f
  with only e ( t*rec ` R ) f
  use biimpi
  use dfrtrclrec2
  use imp
  use rexlimiv
  normalize:ante
conclude E. m e. NN0 f ( R ^r m ) g
  with only f ( t*rec ` R ) g
  use biimpi
  use dfrtrclrec2
  use imp
  use rexlimiv
  normalize:ante
conclude ( <. e , g >. e. ( t*rec ` R ) <-> E. i e. NN0 e ( R ^r i ) g )
  use bitrd
    let $ch = e ( t*rec ` R ) g
    use bicomi
    use df-br
  use dfrtrclrec2
  and rewrite
conclude ( n + m ) e. NN0
  with ( n e. NN0 /\ m e. NN0 )
    use nn0addcl
conclude e ( R ^r ( n + m ) ) g
  conclude ( R ^r ( n + m ) ) = ( ( R ^r m ) o. ( R ^r n ) )
    use eqcomd
    conclude ( n + m ) = ( m + n )
      conclude m e. CC
        with only m e. NN0
          use nn0cn
      conclude n e. CC
        with only n e. NN0
          use nn0cn
      with only ( n e. CC /\ m e. CC )
      use addcom
      and rewrite
    with ( m e. NN0 /\ n e. NN0 )
      use relexpadd
    and rewrite
  conclude ( e ( ( R ^r m ) o. ( R ^r n ) ) g <-> E. h ( e ( R ^r n ) h /\ h ( R ^r m ) g ) )
    use brco
    use vex
    use vex
    and rewrite
  with only ( e ( R ^r n ) f /\ f ( R ^r m ) g )
    use cla4ev
      let $A = f
      use vex
      distr:ante
with only ( ( n + m ) e. NN0 /\ e ( R ^r ( n + m ) ) g )
  use rcla4ev
  distr:ante
quit

prove rtrclreclem.min
use ax-gen
autoall
antedisp
normalize:ante
expand df-rtrclrec
conclude ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n )
  use fvmpti2
  distr:ante
  use iunex
  use relexpex
  and rewrite
use iunss
use ralrimi
normalize:ante
under n e. NN0
  use nn0ind
  let $x = i
  let $y = m
  / i = n
    distr:ante
  / i = 0
    distr:ante
  / i = m
    distr:ante
  / i = . m . 1 .
    distr:ante
0
expand relexp0
conclude U. U. R = ( dom R u. ran R )
  conclude Rel R
    use a1i
  with Rel R
    use relfld
  and rewrite
use relexp0
normalize:ante
conclude ( R ^r m ) C_ s
  with ( m e. NN0 /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) )
conclude ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R )
  with m e. NN0
    use relexpsucr
  and rewrite
use sstrd
  let $B = ( ( R ^r m ) o. s )
with R C_ s
  use coss2
use sstrd
let $B = ( s o. s )
with ( R ^r m ) C_ s
  use coss1
quit

prove relexpindlem
autoall
antedisp
nondisj x <=> ps
use 19.21bi
  let $x = x
under n e. NN0
use nn0ind
  let $x = k
  let $y = l
  substitutions
use ax-gen
expand relexp0
conclude E. i ( i = S /\ ph )
  with only ch
    use cla4ev
      let $A = S
  conclude ( ph <-> ch )
  and rewrite
  use bnj1170
conclude S = x
  conclude ( <. S , x >. e. _I /\ S e. U. U. R )
    use opelres
    use df-br
  normalize:ante
  and conclude S _I x
    use df-br
  use ideq
  and rewrite
use imp
use exlimiv
normalize:ante
with ph
  conclude ( ph <-> ps )
    with i = x
  with only ( ph <-> ps )
use relexp0
# induction step begins
normalize:ante
conclude ( A. x ( S ( R ^r l ) x -> ps ) <-> A. i ( S ( R ^r l ) i -> ph ) )
  use bicomi
  use cbval
    conclude ( i = x -> ( ph <-> ps ) )
    and conclude ( ph <-> ps )
      with i = x
    and rewrite
    and rewrite
  and rewrite
use alrimiv
conclude ( R ^r ( l + 1 ) ) = ( R o. ( R ^r l ) )
  with l e. NN0
    use relexpsucl
  and rewrite
normalize:ante
conclude E. j ( S ( R ^r l ) j /\ j R x )
  use brco
use imp
use exlimiv
normalize:ante
conclude A. i ( S ( R ^r l ) i -> ph )
  with l e. NN0
conclude th
  conclude ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) )
    use cbval
      conclude ( ph <-> th )
      and rewrite
      and rewrite
    and rewrite
  conclude ( S ( R ^r l ) j -> th )
    with only A. j ( S ( R ^r l ) j -> th )
      use a4s
  with S ( R ^r l ) j
with th
  with j R x
quit


prove relexpind
autoall
antedisp
nondisj x <=> ps
nondisj X <=> ta
conclude A. x ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) )
  use ax-gen
  use relexpindlem
    let $i = i
    let $j = j
    let $ph = ph
    let $ch = ch
    let $th = th
use imp
use cla4v
  let $A = X
conclude ( ps <-> ta )
  with x = X
and rewrite
and rewrite
use biid
quit

prove rtrclind
autoall
antedisp
conclude ( t* ` R ) = ( t*rec ` R )
  use dfrtrcl2
  and rewrite
conclude E. n e. NN0 S ( R ^r n ) X
  use dfrtrclrec2
with only E. n e. NN0 S ( R ^r n ) X
use rexlimiv
use relexpind
  let $i = i
  let $j = j
  let $x = x
  let $ph = ph
  let $ch = ch
  let $ps = ps
  let $th = th
quit

prove rtrclreclem.reflexive
autoall
antedisp
expand df-rtrclrec
conclude ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n )
  use fvmpti2
  distr:ante
  use iunex
  use relexpex
  and rewrite
use ssiun
conclude ( _I |` U. U. R ) C_ ( R ^r 0 )
  expand relexp0
  use ssid
conclude 0 e. NN0
  use 0nn0
use rcla4e
and rewrite
quit

prove dfrtrcl2
autoall
antedisp
expand df-rtrcl
conclude ( { <. x , y >. | y = |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } } ` R ) = |^| { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) }
  use fvopab
  use intex
  conclude ( t*rec ` R ) e. { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) }
    use mpbi
      let $ph = ( ( _I |` ( dom R u. ran R ) ) C_ ( t*rec ` R ) /\ R C_ ( t*rec ` R ) /\ ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) )
    use 3pm3.2i
    conclude ( dom R u. ran R ) = U. U. R
      use eqcomi
      use relfld
    and rewrite
    use rtrclreclem.refl
    use rtrclreclem.subset
    use rtrclreclem.trans
    use bicomi
    use elab
    use fvex
    and rewrite
  use ne0i
  use intex
and rewrite
and rewrite
use eqssi
conclude ( t*rec ` R ) e. { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) }
  use intss1
use ssint
  let $x = s
  1
  use ssint
use df-ral
use ax-gen
conclude ( s e. { z | ( ( _I |` ( dom R u. ran R ) ) C_ z /\ R C_ z /\ ( z o. z ) C_ z ) } <-> ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) )
  use elab
  use vex
  and rewrite
  and rewrite
use a4i
  let $x = s
use rtrclreclem.min
quit