:: AMI_4 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K6(NAT) is set
K6(NAT) is set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
K126(9) is Element of K6(NAT)
K191() is set
K198() is set
K6(K198()) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
K7(K198(),2) is Relation-like set
K6(K7(K198(),2)) is set
K200() is Relation-like K198() -defined 2 -valued Function-like V40(K198(),2) Element of K6(K7(K198(),2))
K201() is Relation-like 2 -defined Function-like total set
K200() * K201() is Relation-like K198() -defined set
K180((K200() * K201())) is set
K192() is non empty set
K152(K180((K200() * K201())),K180((K200() * K201()))) is set
K7(K192(),K152(K180((K200() * K201())),K180((K200() * K201())))) is Relation-like set
K6(K7(K192(),K152(K180((K200() * K201())),K180((K200() * K201()))))) is set
SCM is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
the InstructionsF of SCM is non empty Relation-like V72() V73() V74() V76() set
the carrier of SCM is non empty set
K286(2,SCM) is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like V40( the carrier of SCM,2) Element of K6(K7( the carrier of SCM,2))
K7( the carrier of SCM,2) is Relation-like set
K6(K7( the carrier of SCM,2)) is set
the U7 of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the U7 of SCM is Relation-like the carrier of SCM -defined set
RAT is set
INT is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
IC is V51( SCM ) Element of the carrier of SCM
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
{{},1,2,3,4} is finite set
dl. 0 is V63() Element of the carrier of SCM
dl. 1 is V63() Element of the carrier of SCM
dl. 2 is V63() Element of the carrier of SCM
(dl. 2) := (dl. 1) is Element of the InstructionsF of SCM
0 .--> ((dl. 2) := (dl. 1)) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{0} is non empty finite V32() set
{0} --> ((dl. 2) := (dl. 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM -valued {((dl. 2) := (dl. 1))} -valued Function-like constant finite total V40({0},{((dl. 2) := (dl. 1))}) Element of K6(K7({0},{((dl. 2) := (dl. 1))}))
{((dl. 2) := (dl. 1))} is non empty finite set
K7({0},{((dl. 2) := (dl. 1))}) is Relation-like finite set
K6(K7({0},{((dl. 2) := (dl. 1))})) is finite V32() set
Divide ((dl. 0),(dl. 1)) is Element of the InstructionsF of SCM
1 .--> (Divide ((dl. 0),(dl. 1))) is V2() Relation-like NAT -defined {1} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{1} is non empty finite V64() V65() set
{1} --> (Divide ((dl. 0),(dl. 1))) is non empty Relation-like {1} -defined the InstructionsF of SCM -valued {(Divide ((dl. 0),(dl. 1)))} -valued Function-like constant finite total V40({1},{(Divide ((dl. 0),(dl. 1)))}) Element of K6(K7({1},{(Divide ((dl. 0),(dl. 1)))}))
{(Divide ((dl. 0),(dl. 1)))} is non empty finite set
K7({1},{(Divide ((dl. 0),(dl. 1)))}) is Relation-like finite set
K6(K7({1},{(Divide ((dl. 0),(dl. 1)))})) is finite V32() set
(dl. 0) := (dl. 2) is Element of the InstructionsF of SCM
2 .--> ((dl. 0) := (dl. 2)) is V2() Relation-like NAT -defined {2} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{2} is non empty finite V64() V65() set
{2} --> ((dl. 0) := (dl. 2)) is non empty Relation-like {2} -defined the InstructionsF of SCM -valued {((dl. 0) := (dl. 2))} -valued Function-like constant finite total V40({2},{((dl. 0) := (dl. 2))}) Element of K6(K7({2},{((dl. 0) := (dl. 2))}))
{((dl. 0) := (dl. 2))} is non empty finite set
K7({2},{((dl. 0) := (dl. 2))}) is Relation-like finite set
K6(K7({2},{((dl. 0) := (dl. 2))})) is finite V32() set
(dl. 1) >0_goto 0 is Element of the InstructionsF of SCM
3 .--> ((dl. 1) >0_goto 0) is V2() Relation-like NAT -defined {3} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{3} is non empty finite V64() V65() set
{3} --> ((dl. 1) >0_goto 0) is non empty Relation-like {3} -defined the InstructionsF of SCM -valued {((dl. 1) >0_goto 0)} -valued Function-like constant finite total V40({3},{((dl. 1) >0_goto 0)}) Element of K6(K7({3},{((dl. 1) >0_goto 0)}))
{((dl. 1) >0_goto 0)} is non empty finite set
K7({3},{((dl. 1) >0_goto 0)}) is Relation-like finite set
K6(K7({3},{((dl. 1) >0_goto 0)})) is finite V32() set
halt SCM is Element of the InstructionsF of SCM
K273( the InstructionsF of SCM) is V75( the InstructionsF of SCM) Element of the InstructionsF of SCM
4 .--> (halt SCM) is V2() Relation-like NAT -defined {4} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{4} is non empty finite V64() V65() set
{4} --> (halt SCM) is non empty Relation-like {4} -defined the InstructionsF of SCM -valued {(halt SCM)} -valued Function-like constant finite total V40({4},{(halt SCM)}) Element of K6(K7({4},{(halt SCM)}))
{(halt SCM)} is non empty finite set
K7({4},{(halt SCM)}) is Relation-like finite set
K6(K7({4},{(halt SCM)})) is finite V32() set
(3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
(2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
(1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
(0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
() is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
dom () is finite set
dom (3 .--> ((dl. 1) >0_goto 0)) is V2() finite set
dom (4 .--> (halt SCM)) is V2() finite set
dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) is finite set
{3} \/ {4} is non empty finite V64() V65() set
{3,4} is non empty finite V64() V65() set
dom (1 .--> (Divide ((dl. 0),(dl. 1)))) is V2() finite set
dom (2 .--> ((dl. 0) := (dl. 2))) is V2() finite set
dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) is finite set
{2} \/ {3,4} is non empty finite V64() V65() set
{2,3,4} is finite V64() set
dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) is finite set
{1} \/ {2,3,4} is non empty finite V64() V65() set
{1,2,3,4} is finite V64() set
dom (0 .--> ((dl. 2) := (dl. 1))) is V2() finite set
dom ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) is finite set
{0} \/ {1,2,3,4} is non empty finite set
q is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
q . 0 is Element of the InstructionsF of SCM
q . 1 is Element of the InstructionsF of SCM
q . 2 is Element of the InstructionsF of SCM
q . 3 is Element of the InstructionsF of SCM
dom (4 .--> (halt SCM)) is V2() finite set
dom (3 .--> ((dl. 1) >0_goto 0)) is V2() finite set
dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) is finite set
{3} \/ {4} is non empty finite V64() V65() set
{3,4} is non empty finite V64() V65() set
dom (2 .--> ((dl. 0) := (dl. 2))) is V2() finite set
dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) is finite set
{2} \/ {3,4} is non empty finite V64() V65() set
{2,3,4} is finite V64() set
dom (1 .--> (Divide ((dl. 0),(dl. 1)))) is V2() finite set
dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) is finite set
{1} \/ {2,3,4} is non empty finite V64() V65() set
{1,2,3,4} is finite V64() set
dom ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) is finite set
((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) . 0 is set
(0 .--> ((dl. 2) := (dl. 1))) . 0 is set
((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) . 1 is set
(1 .--> (Divide ((dl. 0),(dl. 1)))) . 1 is set
((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) . 2 is set
(2 .--> ((dl. 0) := (dl. 2))) . 2 is set
((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) . 3 is set
(3 .--> ((dl. 1) >0_goto 0)) . 3 is set
q . 4 is Element of the InstructionsF of SCM
((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) . 4 is set
(4 .--> (halt SCM)) . 4 is set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 2) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec (((dl. 2) := (dl. 1)),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 2) := (dl. 1))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 2) := (dl. 1))) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
((Comput (p,q,x)) . (dl. 0)) div ((Comput (p,q,x)) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (p,q,x)) . (dl. 0)) mod ((Comput (p,q,x)) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 2) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec ((Divide ((dl. 0),(dl. 1))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(Divide ((dl. 0),(dl. 1)))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(Divide ((dl. 0),(dl. 1)))) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 2) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 2) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec (((dl. 0) := (dl. 2)),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 0) := (dl. 2))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 0) := (dl. 2))) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec (((dl. 1) >0_goto 0),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 1) >0_goto 0)) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 1) >0_goto 0)) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
x + i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(x + i1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
p is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
p . (dl. 0) is V11() V12() integer ext-real set
p . (dl. 1) is V11() V12() integer ext-real set
x is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Comput (x,p,(4 * q)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * q))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * q))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * q))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * q))) . (IC ) is set
IC p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
p . (IC ) is set
i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (x,p,(4 * i1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * i1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * i1))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * i1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * i1))) . (IC ) is set
i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (i1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (x,p,(4 * (i1 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * (i1 + 1)))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * (i1 + 1)))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * (i1 + 1)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * (i1 + 1)))) . (IC ) is set
(4 * i1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * i1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * i1) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 3)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * i1) + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * i1) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * i1) + 2) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * i1) + 3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * i1) + 3) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * i1) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * i1) + 1) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * i1) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 1))) . (IC ) is set
IC (Comput (x,p,((4 * i1) + 2))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 2))) . (IC ) is set
IC (Comput (x,p,((4 * i1) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 3))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 3))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 2))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 2))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 1))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (x,p,((4 * i1) + 1))) . (dl. 0)) mod ((Comput (x,p,((4 * i1) + 1))) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 1))) . (dl. 2) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (x,p,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * 0))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * 0))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * 0))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * 0))) . (IC ) is set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (q + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
p is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
p . (dl. 0) is V11() V12() integer ext-real set
p . (dl. 1) is V11() V12() integer ext-real set
x is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Comput (x,p,(4 * q)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * q))) . (dl. 1) is V11() V12() integer ext-real set
Comput (x,p,(4 * (q + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * (q + 1)))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * (q + 1)))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,(4 * q))) . (dl. 0) is V11() V12() integer ext-real set
((Comput (x,p,(4 * q))) . (dl. 0)) mod ((Comput (x,p,(4 * q))) . (dl. 1)) is V11() V12() integer ext-real set
(4 * q) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * q) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * q) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 3)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,(4 * q))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * q))) . (IC ) is set
((4 * q) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * q) + 1) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * q) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * q) + 1))) . (IC ) is set
(Comput (x,p,((4 * q) + 2))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 1))) . (dl. 2) is V11() V12() integer ext-real set
((4 * q) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * q) + 2) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * q) + 2))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * q) + 2))) . (IC ) is set
(4 * q) + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * q) + 3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * q) + 3) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * q) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * q) + 3))) . (IC ) is set
(Comput (x,p,((4 * q) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 3))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 2))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 1))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (x,p,((4 * q) + 1))) . (dl. 0)) mod ((Comput (x,p,((4 * q) + 1))) . (dl. 1)) is V11() V12() integer ext-real set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
q . (dl. 0) is V11() V12() integer ext-real set
q . (dl. 1) is V11() V12() integer ext-real set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Result (p,q) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Result (p,q)) . (dl. 0) is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
i1 is V11() V12() integer ext-real set
x gcd i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * i2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * i2))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * i2))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (i2 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * (i2 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * (i2 + 1)))) . (dl. 0) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * (i2 + 1)))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * i2))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,(4 * (i2 + 1)))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * (i2 + 1)))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((Comput (p,q,(4 * i2))) . (dl. 0)) mod ((Comput (p,q,(4 * i2))) . (dl. 1)) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * i2))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
H₂(i2) mod H₁(i2) is V11() V12() integer ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (p,q,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * 0))) . (dl. 0) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * 0))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
abs x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * 0))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * 0))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
abs i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 gcd d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * t)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * t))) . (dl. 0) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * t))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * t))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * t))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
IC (Comput (p,q,(4 * t))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * t))) . (IC ) is set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
q . (dl. 0) is V11() V12() integer ext-real set
q . (dl. 1) is V11() V12() integer ext-real set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Result (p,q) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Result (p,q)) . (dl. 0) is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
i1 is V11() V12() integer ext-real set
x gcd i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
abs i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,4) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (p,q,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
t is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * (0 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
x mod i1 is V11() V12() integer ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 mod d is V11() V12() integer ext-real set
t . (dl. 1) is V11() V12() integer ext-real set
IC t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
t . (IC ) is set
t . (dl. 0) is V11() V12() integer ext-real set
Comput (p,q,4) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
t is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * (0 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (p,q,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
t . (dl. 0) is V11() V12() integer ext-real set
x mod i1 is V11() V12() integer ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 mod d is V11() V12() integer ext-real set
t . (dl. 1) is V11() V12() integer ext-real set
IC t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
t . (IC ) is set
T is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,t,T) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,t,T)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,t,T)) . (IC ) is set
T + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(T + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(T + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(T + 4))) . (IC ) is set
Result (p,t) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Result (p,t)) . (dl. 0) is V11() V12() integer ext-real set
FinPartSt SCM is non empty Element of K6(K184(K286(2,SCM)))
K184(K286(2,SCM)) is set
K6(K184(K286(2,SCM))) is set
{ b₁ where b₁ is Element of K184(K286(2,SCM)) : b₁ is finite } is set
K7((FinPartSt SCM),(FinPartSt SCM)) is Relation-like set
K6(K7((FinPartSt SCM),(FinPartSt SCM))) is set
q is set
p is set
x is set
i1 is V11() V12() integer ext-real set
i2 is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i1,i2) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i1 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i1 is non empty Relation-like {(dl. 0)} -defined {i1} -valued Function-like constant finite total V40({(dl. 0)},{i1}) Element of K6(K7({(dl. 0)},{i1}))
{i1} is non empty finite set
K7({(dl. 0)},{i1}) is Relation-like finite set
K6(K7({(dl. 0)},{i1})) is finite V32() set
(dl. 1) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> i2 is non empty Relation-like {(dl. 1)} -defined {i2} -valued Function-like constant finite total V40({(dl. 1)},{i2}) Element of K6(K7({(dl. 1)},{i2}))
{i2} is non empty finite set
K7({(dl. 1)},{i2}) is Relation-like finite set
K6(K7({(dl. 1)},{i2})) is finite V32() set
((dl. 0) .--> i1) +* ((dl. 1) .--> i2) is Relation-like the carrier of SCM -defined Function-like finite set
i1 gcd i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i1 gcd i2) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i1 gcd i2) is non empty Relation-like {(dl. 0)} -defined {(i1 gcd i2)} -valued Function-like constant finite total V40({(dl. 0)},{(i1 gcd i2)}) Element of K6(K7({(dl. 0)},{(i1 gcd i2)}))
{(i1 gcd i2)} is non empty finite set
K7({(dl. 0)},{(i1 gcd i2)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i1 gcd i2)})) is finite V32() set
d is V11() V12() integer ext-real set
t is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (d,t) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> d is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} --> d is non empty Relation-like {(dl. 0)} -defined {d} -valued Function-like constant finite total V40({(dl. 0)},{d}) Element of K6(K7({(dl. 0)},{d}))
{d} is non empty finite set
K7({(dl. 0)},{d}) is Relation-like finite set
K6(K7({(dl. 0)},{d})) is finite V32() set
(dl. 1) .--> t is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} --> t is non empty Relation-like {(dl. 1)} -defined {t} -valued Function-like constant finite total V40({(dl. 1)},{t}) Element of K6(K7({(dl. 1)},{t}))
{t} is non empty finite set
K7({(dl. 1)},{t}) is Relation-like finite set
K6(K7({(dl. 1)},{t})) is finite V32() set
((dl. 0) .--> d) +* ((dl. 1) .--> t) is Relation-like the carrier of SCM -defined Function-like finite set
d gcd t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (d gcd t) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (d gcd t) is non empty Relation-like {(dl. 0)} -defined {(d gcd t)} -valued Function-like constant finite total V40({(dl. 0)},{(d gcd t)}) Element of K6(K7({(dl. 0)},{(d gcd t)}))
{(d gcd t)} is non empty finite set
K7({(dl. 0)},{(d gcd t)}) is Relation-like finite set
K6(K7({(dl. 0)},{(d gcd t)})) is finite V32() set
(((dl. 0),(dl. 1)) --> (i1,i2)) . (dl. 1) is set
(((dl. 0),(dl. 1)) --> (i1,i2)) . (dl. 0) is set
q is Relation-like Function-like set
rng q is set
p is set
x is set
[x,p] is set
{x,p} is non empty finite set
{x} is non empty finite set
{{x,p},{x}} is non empty finite V32() V64() V65() set
i1 is V11() V12() integer ext-real set
i2 is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i1,i2) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i1 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i1 is non empty Relation-like {(dl. 0)} -defined {i1} -valued Function-like constant finite total V40({(dl. 0)},{i1}) Element of K6(K7({(dl. 0)},{i1}))
{i1} is non empty finite set
K7({(dl. 0)},{i1}) is Relation-like finite set
K6(K7({(dl. 0)},{i1})) is finite V32() set
(dl. 1) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> i2 is non empty Relation-like {(dl. 1)} -defined {i2} -valued Function-like constant finite total V40({(dl. 1)},{i2}) Element of K6(K7({(dl. 1)},{i2}))
{i2} is non empty finite set
K7({(dl. 1)},{i2}) is Relation-like finite set
K6(K7({(dl. 1)},{i2})) is finite V32() set
((dl. 0) .--> i1) +* ((dl. 1) .--> i2) is Relation-like the carrier of SCM -defined Function-like finite set
i1 gcd i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i1 gcd i2) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i1 gcd i2) is non empty Relation-like {(dl. 0)} -defined {(i1 gcd i2)} -valued Function-like constant finite total V40({(dl. 0)},{(i1 gcd i2)}) Element of K6(K7({(dl. 0)},{(i1 gcd i2)}))
{(i1 gcd i2)} is non empty finite set
K7({(dl. 0)},{(i1 gcd i2)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i1 gcd i2)})) is finite V32() set
dom q is set
p is set
q . p is set
[p,(q . p)] is set
{p,(q . p)} is non empty finite set
{p} is non empty finite set
{{p,(q . p)},{p}} is non empty finite V32() V64() V65() set
p is Relation-like FinPartSt SCM -defined FinPartSt SCM -valued Function-like Element of K6(K7((FinPartSt SCM),(FinPartSt SCM)))
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
i1 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
[x,i1] is set
{x,i1} is non empty finite V32() set
{x} is non empty finite V32() set
{{x,i1},{x}} is non empty finite V32() V64() V65() set
i2 is V11() V12() integer ext-real set
d is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i2,d) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i2 is non empty Relation-like {(dl. 0)} -defined {i2} -valued Function-like constant finite total V40({(dl. 0)},{i2}) Element of K6(K7({(dl. 0)},{i2}))
{i2} is non empty finite set
K7({(dl. 0)},{i2}) is Relation-like finite set
K6(K7({(dl. 0)},{i2})) is finite V32() set
(dl. 1) .--> d is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> d is non empty Relation-like {(dl. 1)} -defined {d} -valued Function-like constant finite total V40({(dl. 1)},{d}) Element of K6(K7({(dl. 1)},{d}))
{d} is non empty finite set
K7({(dl. 1)},{d}) is Relation-like finite set
K6(K7({(dl. 1)},{d})) is finite V32() set
((dl. 0) .--> i2) +* ((dl. 1) .--> d) is Relation-like the carrier of SCM -defined Function-like finite set
i2 gcd d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i2 gcd d) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i2 gcd d) is non empty Relation-like {(dl. 0)} -defined {(i2 gcd d)} -valued Function-like constant finite total V40({(dl. 0)},{(i2 gcd d)}) Element of K6(K7({(dl. 0)},{(i2 gcd d)}))
{(i2 gcd d)} is non empty finite set
K7({(dl. 0)},{(i2 gcd d)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i2 gcd d)})) is finite V32() set
q is Relation-like FinPartSt SCM -defined FinPartSt SCM -valued Function-like Element of K6(K7((FinPartSt SCM),(FinPartSt SCM)))
p is Relation-like FinPartSt SCM -defined FinPartSt SCM -valued Function-like Element of K6(K7((FinPartSt SCM),(FinPartSt SCM)))
x is Element of FinPartSt SCM
i1 is Element of FinPartSt SCM
[x,i1] is set
{x,i1} is non empty finite set
{x} is non empty finite set
{{x,i1},{x}} is non empty finite V32() V64() V65() set
i2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
d is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
t is V11() V12() integer ext-real set
T is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (t,T) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> t is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> t is non empty Relation-like {(dl. 0)} -defined {t} -valued Function-like constant finite total V40({(dl. 0)},{t}) Element of K6(K7({(dl. 0)},{t}))
{t} is non empty finite set
K7({(dl. 0)},{t}) is Relation-like finite set
K6(K7({(dl. 0)},{t})) is finite V32() set
(dl. 1) .--> T is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non