Prova:
{ true } [atribui(x, num(0)), atribui(a, false), while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [atribui(x, num(0))] { true } { true } [atribui(a, false), while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [atribui(a, false)] { true } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( true and not ( x < 10 ) ) } { ( true and ( x < 10 ) ) } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))] { true } { ( true and ( x < 10 ) ) } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))])] { true } { ( ( true and ( x < 10 ) ) and a ) } [atribui(x, expInt(soma, ide(x), num(1)))] { true } ( ( ( true and ( x < 10 ) ) and a ) => true ) { true } [atribui(x, expInt(soma, ide(x), num(1)))] { true } ( ( ( true and ( x < 10 ) ) and not a ) => true ) { true } [atribui(a, neg(ide(a)))] { true } ( ( true and not ( x < 10 ) ) => ( x = 10 ) )Sentenças a serem provadas:
( ( true and not ( x < 10 ) ) => ( x = 10 ) ) ( ( ( true and ( x < 10 ) ) and not a ) => true ) ( ( ( true and ( x < 10 ) ) and a ) => true )Prova:
{ true } [atribui(x, num(0)), atribui(a, false), while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [atribui(x, num(0))] { true } { true } [atribui(a, false), while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [atribui(a, false)] { true } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( true and not ( x < 10 ) ) } { ( true and ( x < 10 ) ) } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))] { true } { ( true and ( x < 10 ) ) } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))])] { true } ( ( true and ( x < 10 ) ) => a ) { a } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))])] { true } { ( a and a ) } [atribui(x, expInt(soma, ide(x), num(1)))] { true } ( ( a and a ) => true ) { true } [atribui(x, expInt(soma, ide(x), num(1)))] { true } ( ( a and not a ) => true ) { true } [atribui(a, neg(ide(a)))] { true } ( ( true and not ( x < 10 ) ) => ( x = 10 ) )Sentenças a serem provadas:
( ( true and not ( x < 10 ) ) => ( x = 10 ) ) ( ( true and ( x < 10 ) ) => a ) ( ( a and not a ) => true ) ( ( a and a ) => true )Prova:
{ true } [atribui(x, num(0)), atribui(a, false), while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [atribui(x, num(0))] { true } { true } [atribui(a, false), while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [atribui(a, false)] { true } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( x = 10 ) } { true } [while(expBool(menor, ide(x), num(10)), [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))])] { ( true and not ( x < 10 ) ) } { ( true and ( x < 10 ) ) } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))]), atribui(a, neg(ide(a)))] { true } { ( true and ( x < 10 ) ) } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))])] { true } ( ( true and ( x < 10 ) ) => not a ) { not a } [if(ide(a), [atribui(x, expInt(soma, ide(x), num(1)))])] { true } { ( not a and a ) } [atribui(x, expInt(soma, ide(x), num(1)))] { true } ( ( not a and a ) => true ) { true } [atribui(x, expInt(soma, ide(x), num(1)))] { true } ( ( not a and not a ) => true ) { true } [atribui(a, neg(ide(a)))] { true } ( ( true and not ( x < 10 ) ) => ( x = 10 ) )Sentenças a serem provadas:
( ( true and not ( x < 10 ) ) => ( x = 10 ) ) ( ( true and ( x < 10 ) ) => not a ) ( ( not a and not a ) => true ) ( ( not a and a ) => true )