72 for(
int a=0; a<(int)
d_str.size(); a++ ){
74 sum +=
d_str[a].length();
75 if( a<(
int)
d_pf.size() )
82 for(
int a=0; a<(int)
d_str.size(); a++ ){
84 if( a<(
int)
d_pf.size() ){
85 d_pf[a]->print( s,
d_pf.size()<3 ? ind+1 : 0 );
92 vector< RefPtr< LFSCProof > > d_pfs;
93 d_pfs.push_back( sub_pf );
94 vector< string > d_strs;
95 d_strs.push_back( str_pre );
96 d_strs.push_back( str_post );
102 vector< RefPtr< LFSCProof > > d_pfs;
103 d_pfs.push_back( sub_pf1 );
104 d_pfs.push_back( sub_pf2 );
105 vector< string > d_strs;
106 string str_empty(
" ");
107 d_strs.push_back( str_pre );
108 d_strs.push_back( str_empty );
109 d_strs.push_back( str_post );
115 vector< RefPtr< LFSCProof > > d_pfs;
116 vector< string > d_strs;
118 d_strs.push_back( str );
125 bool isTh, std::vector< int >& fv ) :
LFSCProof(), d_letPf( letPf ),
126 d_pv( pv ),d_body( body ),d_isTh( isTh ){
129 #ifndef IGNORE_LETPF_VARS
131 for(
int a=0; a<(int)fv.size(); a++ ){
132 ostringstream os1, os2;
134 os1 <<
"(impl_intro _ _ ";
143 for(
int a=(
int)fv.size()-1; a>=0; a-- ){
144 ostringstream os1, os2;
145 os1 <<
"(impl_elim _ _ ";
158 s <<
"(" << (
d_isTh ?
"th_let_pf _ " :
"satlem _ _ _ " );