deffunc H_{1}( Vertex of IIG) -> Element of Result ((action_at $1),SCS) = (Den ((action_at $1),SCS)) . ((action_at $1) depends_on_in s);

deffunc H_{2}( set ) -> set = s . $1;

defpred S_{1}[ set ] means $1 in InputVertices IIG;

consider f being ManySortedSet of the carrier of IIG such that

A1: for v being Vertex of IIG st v in the carrier of IIG holds

( ( S_{1}[v] implies f . v = H_{2}(v) ) & ( not S_{1}[v] implies f . v = H_{1}(v) ) )
from PRE_CIRC:sch 2();

then reconsider f = f as State of SCS by A2, CARD_3:def 5;

take f ; :: thesis: for v being Vertex of IIG holds

( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )

let v be Vertex of IIG; :: thesis: ( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )

thus ( v in InputVertices IIG implies f . v = s . v ) by A1; :: thesis: ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) )

A5: InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;

assume v in InnerVertices IIG ; :: thesis: f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s)

then not v in InputVertices IIG by A5, XBOOLE_0:3;

hence f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1; :: thesis: verum

deffunc H

defpred S

consider f being ManySortedSet of the carrier of IIG such that

A1: for v being Vertex of IIG st v in the carrier of IIG holds

( ( S

A2: now :: thesis: for x being object st x in dom the Sorts of SCS holds

f . x in the Sorts of SCS . x

( dom f = the carrier of IIG & dom the Sorts of SCS = the carrier of IIG )
by PARTFUN1:def 2;f . x in the Sorts of SCS . x

let x be object ; :: thesis: ( x in dom the Sorts of SCS implies f . b_{1} in the Sorts of SCS . b_{1} )

assume x in dom the Sorts of SCS ; :: thesis: f . b_{1} in the Sorts of SCS . b_{1}

then reconsider v = x as Vertex of IIG by PARTFUN1:def 2;

end;assume x in dom the Sorts of SCS ; :: thesis: f . b

then reconsider v = x as Vertex of IIG by PARTFUN1:def 2;

per cases
( v in InputVertices IIG or not v in InputVertices IIG )
;

end;

suppose A3:
not v in InputVertices IIG
; :: thesis: f . b_{1} in the Sorts of SCS . b_{1}

v in the carrier of IIG
;

then v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;

then v in InnerVertices IIG by A3, XBOOLE_0:def 3;

then A4: the_result_sort_of (action_at v) = v by MSAFREE2:def 7;

f . x = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1, A3;

hence f . x in the Sorts of SCS . x by A4, CIRCUIT1:8; :: thesis: verum

end;then v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;

then v in InnerVertices IIG by A3, XBOOLE_0:def 3;

then A4: the_result_sort_of (action_at v) = v by MSAFREE2:def 7;

f . x = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1, A3;

hence f . x in the Sorts of SCS . x by A4, CIRCUIT1:8; :: thesis: verum

then reconsider f = f as State of SCS by A2, CARD_3:def 5;

take f ; :: thesis: for v being Vertex of IIG holds

( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )

let v be Vertex of IIG; :: thesis: ( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )

thus ( v in InputVertices IIG implies f . v = s . v ) by A1; :: thesis: ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) )

A5: InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;

assume v in InnerVertices IIG ; :: thesis: f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s)

then not v in InputVertices IIG by A5, XBOOLE_0:3;

hence f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1; :: thesis: verum